Autonomic software-intensive systems: foundations of safety and resilience

The project aims at developing a framework for designing autonomous safety-critical systems. It should provide software-intensive systems with capabilities to monitor their behaviour and, upon detecting off-nominal situations, autonomously diagnose their causes and adapt to new conditions. Our goal is to enhance safety and resilience of critical software-intensive systems. By integrating monitoring and adaptability into the system we would allow it to adjust to unforeseen circumstances and maintain its operation. Moreover, this approach would also enhance resilience of a system by enabling it to evolve together with its operational environment.

Software-intensive systems are becoming widely used in such critical infrastructures as railway, air-, and road traffic, power management, health care and banking. Over the last decade complexity of software has reached unprecedented level, thus making exhaustive testing of system properties unfeasible. Can we justifiably put our trust on critical software-intensive systems? The idea of this project is inspired by the autonomic computing paradigm. We aim at creating a formal basis for a novel framework of system health management. The framework should provide software-intensive systems with capabilities to monitor their behaviour and, upon detecting off-nominal situations, autonomously diagnose their causes and adapt to new conditions. Our goal is to enhance safety and resilience of critical software-intensive systems. By integrating monitoring and adaptability into the system we would allow it to adjust to unforeseen circumstances and maintain its operation. Moreover, this approach would also enhance resilience of a system by enabling it to evolve together with its operational environment. To create a theoretic basis of software health management, we propose to integrate three different frameworks: system modelling by refinement, run-time verification and probabilistic methods for fault diagnosis. To monitor the system behaviour and detect off-nominal situations, we need a model of nominal system behaviour. Development paradigm based on refinement and our work on integrating it with reasoning about safety can provide us with such a model. As a result of refinement we obtain a detailed system model that can be used as an input for monitoring. Monitoring can be actually implemented as run-time verification using a SAT-solver. The SAT-solver would detect off-nominal situations by discovering refuted invariants. Then the health monitoring subsystem would try to find a strategy for recovery and adaptation. Finally, probabilistic methods based on Markov decision processes can be used to diagnose problems and find an optimal recovery strategy. Overall, such an approach amplifies benefits of the integrated frameworks: reasoning about system properties at different levels of abstraction provided by the refinement approach, efficient checking of property preservation provided by SAT-solvers and advanced methods for fault diagnosis and mitigation provided by probabilistic methods. We believe that synergy of these frameworks will provide a significant impact on the field of critical software-intensive systems.