Self-adaptive automata.

Self-adaptive systems aim to efficiently respond to a wide range of changes in their operational environment by dynamically altering their behaviour. Such systems are typically comprised of a base system, implementing core functionality, and an adaptation decision process, which determines how the base system must change at different points in its execution. These two components coordinate through a set of adaptation events: a set of execution points of the former where the latter is invoked. The pattern of these events is crucial for the overall system to achieve (a) correctness against specific requirements, and (b) efficiency of system resources. Existing techniques for modelling self-adaptive systems usually hardcode adaptation events within the base system or the adaptation decision process. This limits system designers in discovering correct and optimal patterns of adaptation events, as changing those involves significant changes in the model. In this work we present Self-Adaptive Automata, an abstract modelling framework which decouples adaptation event patterns from the descriptions of base systems and adaptation decision processes. In our framework, base systems expose execution points where adaptation may happen---in the most general case this can include all system states---and adaptation decision processes are parametric to these points. A distinct automaton then pinpoints when in the system adaptation must happen. Using this framework system designers can experiment with different adaptation event patterns, without modifications to the base system or the adaptation decision process, and discover correct and efficient patterns. We show that our framework is compatible with traditional verification tools by providing an adequate translation from Self-Adaptive Automata into FDR, in which correctness against requirements can be verified. We also prove that, although our automata framework includes dynamic self-modifying features, it corresponds to standard models of computation. We illustrate the use of our framework through a use case of a self-adaptive system of autonomous search-and-rescue rovers.