ISBN 978-3-8439-4189-1

978-3-8439-4189-1, Reihe Informatik

Thorsten Ropertz
Design and Analysis of Behavior-Based Systems using Formal Techniques

192 Seiten, Dissertation Technische Universität Kaiserslautern (2019), Softcover, A5

Zusammenfassung / Abstract

In the 1980s, a promising software architecture class called behavior-based systems has been invented, which tries to cope with the high sensory and motor dimension by rigorously applying the divide and conquer principle. In contrast, the classic, usually monolithic control approaches, behavior-based control systems consist of rather simple interacting components which form a network of behaviors. These control systems offer several advantages concerning robustness, fault tolerance, and flexible adaptation due to the partially overlapping functionality and dynamic arbitration process. Unfortunately, behavior-based control networks are challenging to design due to their size and complexity. Since this control approach is applied in safety-critical systems, which could cause severe harm to goods and people, their correctness is however mandatory.

The work at hand presents a novel approach for reducing faults in complex behavior-based control systems. Inspired by the defect causal analysis, typical faults in behavior-based control systems based on the iB2C architecture are analyzed, and measures to prevent or remove them are developed. Thereby, the investigation is divided into two parts:

On the behavior level, the architecture is adapted to guide the developer better and thus prevent faults. Design principles are defined that are necessary for separate analysis. Additionally, the modeling and verification of the actual control algorithm using hybrid system verification techniques to guarantee correctness with respect to its specification are presented.

On the network-level, the network structure and the arbitration process are investigated to detect and prevent typical faults like missing or wrong interconnections. Thereby, the explicit specification of external conditions and priorities among competing behaviors, as well as their integration in a formal graph representation reduces faults by forcing the developer to model the direct and indirect effects of interconnections explicitly. Support of the automatic generation of the network structure from the specification and vice-versa further reduces faults in the development process.

The presented techniques are applied to a real-world application example throughout the whole thesis to discuss their properties and show their applicability.