Game-Based Model Checking for Reliable Autonomy in Space
- 1 April 2011
- journal article
- research article
- Published by American Institute of Aeronautics and Astronautics (AIAA) in Journal of Aerospace Information Systems
- Vol. 8 (4), 100-114
- https://doi.org/10.2514/1.32013
Abstract
Autonomy is an emerging paradigm for the design and implementation of managed services and systems. Self-managed aspects frequently concern the communication of systems with their environment. Self-management subsystems are critical, they should thus be designed and implemented as high-assurance components. Here, we propose to use GEAR, a game-based model checker for the full modal mu-calculus, and derived, more user-oriented logics, as a user friendly tool that can offer automatic proofs of critical properties of such systems. Designers and engineers can interactively investigate automatically generated winning strategies resulting from the games, this way exploring the connection between the property, the system, and the proof. The benefits of the approach are illustrated on a case study that concerns the ExoMars Rover.Keywords
This publication has 6 references indexed in Scilit:
- Tool-supported enhancement of diagnosis in model-driven verificationInnovations in Systems and Software Engineering, 2009
- Model-Driven Development with the jABCPublished by Springer Science and Business Media LLC ,2007
- Lightweight coarse-grained coordination: a scalable system-level approachInternational Journal on Software Tools for Technology Transfer, 2004
- Local model checking games (extended abstract)Lecture Notes in Computer Science, 1995
- On model-checking for fragments of μ-calculusLecture Notes in Computer Science, 1993
- Results on the propositional μ-calculusLecture Notes in Computer Science, 1982