University of Limerick
Browse

Model checking for autonomic systems specified with ASSL

Download (525.4 kB)
conference contribution
posted on 2012-01-11, 15:16 authored by Emil VassevEmil Vassev, Mike Hinchey, Aaron Quigley
Autonomic computing augurs great promise for deep space exploration missions, bringing onboard intelligence and less reliance on control links. As part of our research on the ASSL (Autonomic System Specification Language) framework, we have successfully specified autonomic properties, verified their consistency, and generated prototype models for both the NASA ANTS (Autonomous Nano-Technology Swarm) concept mission and the NASA Voyager mission. The first release of ASSL provides built-in consistency checking and functional testing as the only means of software verification. We discuss our work on model checking autonomic systems specified with ASSL. In our approach, an ASSL specification is translated into a state-transition model, over which model checking is performed to verify whether the ASSL specification satisfies correctness properties. The latter are expressed as temporal logic formulae expressed over sets of ASSL constructs. We also discuss possible solutions to the state-explosion problem in terms of state graph abstraction and probability weights assigned to states. Moreover, we present an example case study involving checking liveness properties of autonomic systems with ASSL

History

Publication

1st NASA Formal Methods Symposium (NFM);2009 pp 16-25

Note

non-peer-reviewed

Other Funding information

SFI

Language

English

Usage metrics

    University of Limerick

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC