Algebraic Calculi for Hybrid Systems

Over the past decades incorrect software has claimed numerous lives and has caused environmental damages. Furthermore incorrect software regularly yields economic losses. Systems that interact with their environment are especially fault-prone. On the one hand, they have to be flexible enough to react to environment changes, on the other hand they have to be predictable. Unlike software systems for office work, interacting systems must satisfy restrictive safety criteria - an airbag that inflates too late is unacceptable. Hybrid systems are often used to model such safety critical systems. They are heterogeneous systems characterised by the interaction of continuous dynamics and discrete events that cause state changes. They have found widespread applications ranging from control and medical engineering to avionics. But even biological and chemical processes can concisely be described by such systems. In many cases, hybrid systems are too complex for computer-aided verification - even with today's computers that offer enormous memory and calculating capacities. In this book, we aim at a compact treatment of verification tasks. Algebraic techniques are of particular interest and arise in a natural way. Systems are algebraically described by systems of equations that are similar to those known from high school. Advantages that accrue by an algebraic approach are conciseness, clarity and simplicity; in particular with respect to (computer-aided) calculation rules. The developed algebraic characterisation of hybrid systems allows, for example, the verification of safety aspects by simple algebraic transformations. The approach further enables the use of off-the-shelf automated theorem provers. These provers can be employed to verify fundamental properties of hybrid systems. Over the last decade dozens of logic-based approaches have been applied to hybrid systems. These approaches range from classical propositional logics and modal or temporal logics that have been transferred over to hybrid systems to special logics that have been developed for them. Most of them are well-understood, but due to their different notions, syntax and semantics a uniform treatment is not available. Therefore we explore a compact and uniform treatment for all these logics. The unification is based on the same algebraic techniques as for the characterisation of hybrid systems. This allows cross-reasoning through all unified logics. In this book we pay special attention to the relationship between the logics involved and hybrid systems. The book presents fundamental methods for the analysis of hybrid systems and results in a coherent family of algebraic calculi for hybrid systems. The suitability and the relevance of the theory is proved by first case studies.Fehlerhafte Software hat in den letzten Jahrzehnten zahlreiche Menschenleben gefordert, Umweltschäden hervorgerufen und regelmäßig zu enormen wirtschaftlichen Verlusten geführt. Besonders fehleranfällig sind hierbei Systeme, welche ständig mit ihrer Umwelt interagieren, da sie auf diese flexibel, aber dennoch vorhersagbar reagieren müssen. Anders als für reine Softwaresysteme wie Büroanwendungen, sind Korrektheitsanforderungen in diesen Bereichen besonders hoch - ein Airbag, der sich zu spät öffnet, ist nicht akzeptabel. Solche sicherheitskritische Systeme können meistens als so genannte hybride Systeme charakterisiert werden. Bei diesen Systemen besteht ein Wechselspiel zwischen kontinuierlichem Systemverhalten und Kontrollereignissen zu diskreten Zeitpunkten, die Zustandswechsel auslösen. Anwendungsgebiete reichen von Steuerungselementen über Medizintechnik bis hin zu Avionik. Aber auch chemische und biologische Systeme können mittels solcher Systeme mathematisch exakt beschrieben werden. Hybride Systeme sind jedoch häufig so komplex, dass eine computergestützte Verifikation auch mit den heute verfügbaren großen Speicher- und Rechenkapazitäten nicht durchführbar ist. Ziel des vorliegenden Buches ist es, Untersuchungen zu einer kompakteren Behandlungsmöglichkeit von Verifikationsaufgaben anzustellen. Zentrales Interesse finden hierbei algebraische Techniken, in denen Systeme durch Gleichungsregeln - ähnlich den aus der Schulalgebra bekannten - beschrieben werden. Die generellen Vorteile eines algebraischen Ansatzes sind vor allem Klarheit und Einfachheit, insbesondere im Hinblick auf (computerunterstützbare) Rechenregeln. Die entwickelte algebraische Charakterisierung hybrider Systeme ermöglicht es beispielsweise, Sicherheitsaspekte mittels einfacher algebraischer Umformungen zu überprüfen. Ferner bietet dieser Ansatz den Vorteil, dass Standard-Computer-Algebrasysteme verwendet werden können. So können Theorembeweiser eingesetzt werden, um fundamentale Eigenschaften hybrider Systeme automatisch zu verifizieren. Im letzten Jahrzehnt wurden Dutzende unterschiedlicher Logiken für hybride Systeme eingesetzt: Angefangen von klassischer Aussagenlogik über modale und temporale Logiken bis hin zu eigens für diese Systeme entwickelten Logiken. Die meisten dieser Logiken sind für sich wohlverstanden. Aber auf Grund der Vielzahl von verwendeten Begriffen sowie ihrer unterschiedlichen Notation und Bedeutung ist eine uniforme Behandlung der Logiken und ihrer Beziehungen zueinander sehr schwierig. In dem vorliegenden Buch werden daher Untersuchungen zu einer kompakteren und einheitlichen Behandlung angestellt. Zentrales Interesse finden hierbei dieselben algebraischen Techniken wie zur Beschreibung von hybriden Systemen. Durch Algebraisierung ist es möglich, Beziehungen zwischen Logiken aufzuzeigen und, für dieses Buch von besonderer Bedeutung, diese Logiken in einer einheitlichen und systematischen Weise auf hybride Systeme anzuwenden. Die Forschungsergebnisse umfassen grundlegende Methoden zur Analyse hybrider Systeme und münden in eine kohärente Familie algebraischer Kalküle für hybride Systeme. Die Anwendbarkeit und Relevanz der Theorie ist durch erste Fallstudien belegt