Loading...
Model checking for autonomic systems specified with ASSL
Date
2009
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
Supervisor
Description
non-peer-reviewed
Publisher
Citation
1st NASA Formal Methods Symposium (NFM);2009 pp 16-25
Files
Loading...
2009_Vassev.pdf
Adobe PDF, 525.4 KB
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)