The SHADOWS Story on Implementation of Self-Healing Systems

by Marco Bakera and Tiziana Margaria

Industry-grade, large-scale software systems have an inherent need for autonomous mechanisms of adaptation. In our approach, a new game-based model-checking technique succeeds as a natural solution to the verification and adaptation task: the system becomes a player in a hostile world, and competes against any potential problems or mishaps.

Figure 1: ExoMars rover - phase B1 concept (courtesy of ESA).

Software self-healing is an emerging approach to addressing the problems of handling and fixing large complex software systems. In the European SHADOWS project on Self-Healing Approach to Designing Complex Software Systems, research institutions (University of Potsdam- D, Milano Bicocca - I, and Brno - CZ, and the IBM Research Labs in Haifa - IL) and industry (Telefonica I&D - E, Net Tech - GR, Artisys - CZ, Israel Avionics Industries - IL) are extending the state of the art for self-healing systems in several dimensions: innovative technology enables self-healing for a wide range of problems not solved elsewhere, several forms of self-healing technology are integrated into a common solution, and a model-based approach enables models of desired software behaviour to direct the self-healing process. This life-cycle support of self-healing is directly applied to industrial systems.

The specific formal verification and adaptation techniques we develop are based on games: they help engineers to describe, design and ensure the functional healing aspects of autonomous system behaviours. For example, once ESA's ExoMars Rover (see Figure 1) is sent on a surface mission on Mars, it must accomplish several tasks, including the acquisition of subsurface soil samples using a drill. If anything goes wrong, it should adequately adapt its behaviour: by reconfiguring itself to complete the task in a different way, choosing a different task it can still perform or at least returning to a basic safe behaviour. With our game-based model-checking approach, engineers can play with a model of the system just as they are accustomed to doing in today's common simulation approaches. However, at the same time they can express, modify and prove the behaviour of the system (the model) and the properties that are required or guaranteed. Hence, this new technique gives them verification, diagnosis and adaptation of temporal properties for free.

Figure 2: Acquire Sample Task as storytelling model - the basis for the game play.

The central acceptance issue for the new technique, based on the GEAR model checker, is that it can be seamlessly integrated with the engineer's working experience. The robot's formal but intuitive behavioural model is created in terms of processes within the jABC framework a mature, model-driven, service-oriented process definition platform. The jABC is also at the core of the FMICS-jETI and Bio-jETI platforms developed at Dortmund/Potsdam within the ERCIM Working Group on Formal Methods for Industrial Critical Systems (FMICS).

This modelling style closely matches the descriptions given by the ExoMars designers: actions are the atomic, Lego-like basic building blocks of the robot's behaviour, tasks are structured as flow graphs of actions, and mission plans are composed of tasks in a similar fashion. This leads to a hierarchical model of the entire behaviour.

The blend of model and property that reveals their interplay in a user-friendly way is a game played by two players: a demonic player (the hostile environment) that tries to refute the property, and an angelic player (the system) that tries to verify it. The result of the game corresponds to the result of the property verification process. The game graphs are at the same interactive counter examples, that reveal problems between specification and implementation in an interactive way, and mathematical proofs. As with a simulator or debugger, commonly used today in integrated development environments, playing the game exposes executions of the system that violate the property. In contrast to ordinary simulation and step-by-step debugging however, which establishes understanding for only one concrete case at a time, the game provides a property-oriented exploration of the model, characterizing all the system behaviours that violate the property.

Used for diagnosis, the game approach fosters a more general and concise understanding of the property violation. Used for repair, the elaborate information on the property violation obtained from the game graph helps engineers to adapt the system or the property, thus realigning them.

Whenever the system violates crucial behavioural properties, the game-based verification and adaptation approach provides a deeper and global behavioural insight into the nature of the problem. Behavioural properties become more demanding for more complex systems; adaptation properties, as addressed in SHADOWS, are very well suited to this game-based abstract exploration of alternatives driven by properties that represent correctness goals.

The quest continues: for more properties, more elaborate adaptation schemes, and for a natural inclusion of the new game-based verification in the everyday experience of engineers.

Links:
SHADOW project: https://sysrun.haifa.il.ibm.com/shadows/
jABC: http://jabc.cs.uni-dortmund.de/
GEAR: http://jabc.cs.uni-dortmund.de/gear
FMICS-jETI: http://eti.informatik.uni-dortmund.de/fmics/
Bio-jETI: http://eti.informatik.uni-dortmund.de/biojeti/

Please contact:
For SHADOWS, FMICS-jETI and Bio-jETI:
Tiziana Margaria
University of Potsdam, Germany
Tel: +49 331 9773040
E-mail: margariacs.uni-potsdam.de