nach oben

2010 | Buch

Kapitel lesen Erstes Kapitel lesen

Logical Analysis of Hybrid Systems

Proving Theorems for Complex Dynamics

verfasst von: André Platzer

Verlag: Springer Berlin Heidelberg

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten

Über dieses Buch

Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical–chemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerized controllers for physical systems which are guaranteed to meet their design goals. The author gives a unique, logic-based perspective on hybrid systems analysis. It is the first book that leverages the power of logic for hybrid systems. The author develops a coherent logical approach for systematic hybrid systems analysis, covering its theory, practice, and applications. It is further shown how the developed verification techniques can be used to study air traffic and railway control systems. This book is intended for researchers, postgraduates, and professionals who are interested in hybrid systems analysis, cyberphysical or embedded systems design, logic and theorem proving, or transportation and automation.

Inhaltsverzeichnis

Frontmatter

Chapter 1. Introduction

Abstract

Ensuring correct functioning of complex physical systems is among the most challenging and most important problems in computer science, mathematics, and engineering. In addition to nontrivial underlying physical system dynamics, the behaviour of complex systems is determined increasingly by computerised control and automatic analog or digital decision-making, e.g., in aviation, railway, and automotive applications. At the same time, correct decisions and control of these systems are becoming increasingly important, because more and more safety-critical processes are regulated using automatic or semiautomatic controllers, including the European Train Control System [117], collision avoidance manoeuvres in air traffic control [293, 196, 104, 238, 129, 171], car platooning technology for highways following the California PATH project [166], recent driverless vehicle technology [64], and biomedical applications like automatic glucose regulation for diabetes patients [223]. As a more general phenomenon of complex physical systems that are exemplified in these scenarios, correct system behaviour depends on correct functioning of the interaction of control with physical system dynamics and is not just an isolated property of only the control logic or only the physical system dynamics. These interactions of computation and control are more difficult to understand and get right than isolated systems. Even if the control software does not crash, the system may still malfunction, because the control software could issue unsafe control actions to the physical process. And even if the pure physics of the process is well understood, an attempt to control the process may still become unsafe, e.g., when the controller reacts to situation changes too slowly because computations take too long, or when sensor values are already outdated once the control actions finally take effect. It is the interaction of computation and control that must be taken into account. Systems with such an interaction of discrete dynamics and continuous dynamics are called hybrid dynamical systems, or just hybrid systems for short.

André Platzer

Logics and Proof Calculi for Hybrid Systems

Frontmatter

Chapter 2. Differential Dynamic Logic dℒ

Synopsis

Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free-variable proof calculus with a novel combination of real-valued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a study with cooperating traffic agents of the European Train Control System, we further show that our calculus is well suited for verifying realistic hybrid systems with parametric system dynamics.

André Platzer

Chapter 3. Differential-Algebraic Dynamic Logic DAL

Synopsis

We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly, including systems with disturbance and differential-algebraic equations. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which differential-algebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them.We develop the theory of differential induction and differential refinement and analyse their deductive power. As an example, we present parametric tangential roundabout manoeuvres in air traffic control and prove collision avoidance in our calculus.

André Platzer

Chapter 4. Differential Temporal Dynamic Logic dTL

Synopsis

We combine first-order dynamic logic for reasoning about the possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with first-order definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of our dynamic logic for hybrid systems. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to nontemporal reasoning, and prove that we obtain a complete axiomatisation relative to the nontemporal base logic. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.

André Platzer

Automated Theorem Proving for Hybrid Systems

Frontmatter

Chapter 5. Deduction Modulo Real Algebra and Computer Algebra

Synopsis

We show how deductive, real algebraic, and computer algebraic methods can be combined for verifying hybrid systems in an automated theorem proving approach. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. Systematically, we derive a canonical tableau procedure modulo from the calculus of differential dynamic logic. We delineate the nondeterminisms in the tableau procedure carefully and analyse their practical impact in the presence of computationally expensive handling of real algebraic constraints. Based on experience with larger case studies, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems. To overcome the complexity pitfalls of integrating real arithmetic, we propose the iterative background closure and iterative inflation order strategies, with which we achieve substantial computational improvements.

André Platzer

Chapter 6. Computing Differential Invariants as Fixed Points

Synopsis

We introduce a fixed-point algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use differential induction as a continuous generalisation of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixed-point algorithm works with differential dynamic logic as a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively by differential cuts with differential invariants until the property becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout manoeuvres in air traffic control and collision avoidance in train control.

André Platzer

Case Studies and Applications in Hybrid Systems Verification

Frontmatter

Chapter 7. European Train Control System

Synopsis

Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For the free parameters of the system, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterising them equivalently in terms of reachability properties of the hybrid system dynamics. We use the calculus of our differential dynamic logic for hybrid systems and formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics.

André Platzer

Chapter 8. Air Traffic Collision Avoidance

Synopsis

Aircraft collision avoidance manoeuvres are important and complex applications.Curved flight exhibits nontrivial continuous behaviour. In combination with the control choices during air traffic manoeuvres, this results in hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study for demonstrating the scalability of logical analysis for hybrid systems with challenging dynamics, we analyse collision freedom of roundabout manoeuvres in air traffic control, where appropriate curved flight, good timing, and compatible manoeuvring are crucial for guaranteeing safe spatial separation of aircraft throughout their flight.We show that our DAL-based proof techniques can scale to curved flight manoeuvres required in aircraft control applications. Our logical analysis approach can be used successfully to verify collision avoidance of the tangential roundabout manoeuvre automatically, even for five aircraft. Moreover, we introduce a fully fly-able variant of the roundabout collision avoidance manoeuvre and verify safety properties by compositional verification in our calculus.

André Platzer

Chapter 9. Conclusion

Abstract

Hybrid systems are an equally important and challenging class of systems, whose numerous occurrences in safety-critical complex physical systems call for formal verification techniques to establish their correct functioning by rigorous mathematical analysis. The characteristic feature of the modelling idea behind hybrid systems is that they admit interacting discrete and continuous dynamics to capture the superposition of physical system dynamics with control at a natural modelling level. With these superpositions, hybrid systems can model challenging system dynamics fairly easily but also require sophisticated analysis techniques.

André Platzer

Backmatter

Titel: Logical Analysis of Hybrid Systems
verfasst von: André Platzer
Verlag: Springer Berlin Heidelberg
Electronic ISBN: 978-3-642-14509-4
Print ISBN: 978-3-642-14508-7
DOI: https://doi.org/10.1007/978-3-642-14509-4