TY  - JOUR
A1  - Bakera, Marco
A1  - Margaria, Tiziana
A1  - Renner, Clemens D.
A1  - Steffen, Bernhard
T1  - Game-Based model checking for reliable autonomy in space
T2  - Journal of aerospace computing, information, and communication
N2  - 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.
Y1  - 2011
UR  - https://publishup.uni-potsdam.de/frontdoor/index/index/docId/37115
SN  - 1940-3151
VL  - 8
IS  - 4
SP  - 100
EP  - 114
PB  - American Institute of Aeronautics and Astronautics
CY  - Reston
ER  -