University of Limerick Institutional Repository

Model checking for autonomic systems specified with ASSL

DSpace Repository

Show simple item record Vassev, Emil Hinchey, Mike Quigley, Aaron 2012-01-11T15:16:45Z 2012-01-11T15:16:45Z 2009
dc.description non-peer-reviewed en_US
dc.description.abstract 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 en_US
dc.language.iso eng en_US
dc.relation.ispartofseries 1st NASA Formal Methods Symposium (NFM);2009 pp 16-25
dc.subject ASSL en_US
dc.subject NASA en_US
dc.subject software en_US
dc.subject computing en_US
dc.title Model checking for autonomic systems specified with ASSL en_US
dc.type Conference item en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.type.restriction none en
dc.contributor.sponsor SFI

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account