Start of the project 2007, end of the project 2016

This project deals with the development of methods for quantifying and extending the properties of self-stabilising systems. In order to enable non-experts to develop self-stabilising systems, such methods must be automated as far as possible. The underlying models for the analysis and re-engineering methods are discrete time Markov chains (DTMC) and discrete time Markov decision processes (DTMDP). One problem of the analysis of self-stabilising systems is based on the fact that the number of possible initial states is equal to the number of all possible states. Therefore, abstraction schemes and semantic models are developed to overcome these problems that occur during the analysis. It is impossible to define a procedure that covers the entire class of self-stabilising systems. Therefore, self-stabilising systems are classified according to their behaviour and proof obligations are elaborated for each subclass. Furthermore, fault tolerance metrics are introduced to quantify the behaviour of self-stabilising systems. Often, the level of fault tolerance that has been announced is not achieved due to a lack of implementation experience for self-stabilising systems. It is therefore important to utilise this knowledge when implementing scenarios. As part of this project, counterexamples generated by analysis methods are used to revise a system so that a specified quality of service is achieved (Figure). Furthermore, the aim is to identify heuristics so that the state space of a scenario in a counterexample can be mapped to a modification protocol to improve fault tolerance metrics.

• Prof. Dr Oliver Theel
• Dr Abhishek Dhama, MSc. CS & CE
• Dr Oday Jubran, MSc. Computing Science