Extracting Component-Oriented Behaviour for Self-Healing Enabling

Rich and multifaceted domain specific specification languages like the Autonomic System Specification Language (ASSL) help to design reliable systems with self-healing capabilities. The GEAR game-based Model Checker has been used successfully to investigate in depth properties of the ESA ExoMars Rover. We show here how to enable GEAR´s game-based verification techniques for ASSL via systematic model extraction from a behavioral subset of the language, and illustrate it on a description of the Voyager II space mission. This way, we close the gap between the design-time and the run-time techniques provided in the SHADOWS platform for self-healing of concurrency, performance, and functional issues.