Behavioural Theory and Logics for Distributed Adaptive Systems

A distributed, adaptive system is a system that is composed of communicating, autonomous components. The behaviour of components may be volatile, i.e. components may break down, become unavailable due to network problems or change their behaviour. Thus, the system has to be adaptive to recognise faulty behaviour, adapt itself to new arising situations if possible, and return to its original processing in case the cause of the problem has been removed. Thus, monitoring the system`s environment and adapting the behaviour to critical situations is a defining characteristic of distributed, adaptive systems. For instance, a production cell may comprise several autonomous systems (e.g. controlling welding robots) to perform a joint task (e.g. a welding task in car production). These systems may communicate with each other to assess, if all components are working properly, and to reach a consensus when the task is considered to be completed. In case one of the components becomes malfunctioning, the remaining components should be able to discover the failure, isolate the component and issue a signal that it has to be replaced, and re-allocate the task among themselves if possible. After the faulty component has been replaced or repaired, which could be signalled to the system, the system could return to the original task allocation before the incident. Various production cells of different kind could form a production line. Then the collection of production cells can be controlled by another distributed adaptive system with more adaptation latitude, e.g. changing the order of tasks, using a support component, etc. This may further be extended to the level of a factory with several production lines, and the whole production of a company that is distributed over many factories. The general aim of the project is to develop solid scientific foundations capturing all aspects of distributed adaptive systems in a step-by-step approach. The project aims at clarifying what exactly distributed adaptive systems are, how they can be specified, how properties such as reliability, resilience and robustness can be guaranteed, and how they can be classified. For this the notion of "behavioural theory" will be adopted from Gurevich`s seminal work on the ASM thesis and follow-on research on language-independent characterisation of classes of algorithms.

A distributed system is a system that is composed of autonomous software components. The components are distributed over a network; they collaborate via shared storage locations and messages. Autonomy of the components means that each component apart from knowing that some storage locations can be updated by others is oblivious to the behaviour of the other components. Such a distributive system is adaptive, if components can change their behaviour, i.e. the program associated with each component can be changed by the system itself. When a component breaks down or becomes unavailable due to network problems or an anomalous component enters the system, others may recognise this behaviour and adapt themselves to the new arising situation. Thus, monitoring the systems environment and adapting the behaviour to critical situations is a defining characteristic of distributed, adaptive systems.For instance, a production cell may comprise several autonomous systems to perform a joint task. These systems may communicate with each other to assess, if all components are working properly, and to reach a consensus when the task is considered to be completed. In case one of the components becomes malfunctioning, the remaining components shall be able to discover the failure, isolate the component, issue a signal that it has to be replaced, and re-allocate the task among themselves if possible. After the faulty component has been replaced or repaired, which can be signalled to the system, the system returns to the original task allocation before the incident.The first key result of the project is a behavioural theory of such distributed adaptive systems. The theory comprises (1) a general language-independent characterisation by a set of intuitive postulates that are satisfied by all known system formalisms, (2) an abstract machine model that provably satisfies the postulates, and (3) the mathematical proof that all systems stipulated by the postulates can be faithfully represented by the abstract machine model. The behavioural theory enables system specifications in general using a concrete language for the abstract machine model.The second key result is a logic for such distributed adaptive systems that is based on the abstract machine model. The logic allows system developers to formally characterise desirable properties that system specifications must meet and to mathematically verify these properties. In particular, static verification with this logic permits to give assertions for states that result after many adaptations of the system.