André Platzer: Logical Analysis of Hybrid Systems
Springer, 2010, 426 pages, ISBN 978-3-642-14508-7
https://link.springer.com/book/10.1007%2F978-3-642-14509-4
Summary
This is an extensive book on deductive methods for hybrid systems’ verification, rooted in dynamic logic. The author develops both formal specification languages for hybrid systems and automated verification techniques based on them. The main focus is on the theoretical aspects of the approach, but implementation issues are also widely addressed, and a functioning tool is presented at the end of the book. It presents a powerful formalism for the specification and verification of hybrid systems, with a strong practical impact.
This review is written by Gabriele Paveri Fontana for FME’s Book Review Committee (BRC). The aim of the BRC is to provide to the formal methods community, and to the scientific community in general, high-quality reviews of books on topics of interest to the community.
Logical Analysis of Hybrid Systems
by
André Platzer.
Review
The book is an extensive presentation of deductive methods for hybrid systems’ verification rooted in dynamic logic. The author develops both formal specification languages for hybrid systems and automated verification techniques based on them. The main focus is on the theoretical aspects of the approach, but implementation issues are also widely addressed, and a functioning tool is presented at the end of the book. The book, which is now a few years old, is based on the Ph.D. thesis of the author, but, especially the more theoretical parts, is still current, as it provides the foundations, for example, of the approach of [1]. Given its origin, the book is certainly of great interest for researchers dealing with hybrid systems, but it is also recommendable for anyone who is interested in the general topics of modeling and verification of complex (timed) systems. A good degree of familiarity with formal methods and mathematical logic is necessary to fully appreciate the contents of the book.
The book is divided into three parts, plus an appendix. Part I focuses on theoretical aspects. The book’s approach stems from the necessity of overcoming several critical issues of standard model checking techniques based on automata models when applied to hybrid systems; to name a few, undecidability arises even with the simplest examples, approximation techniques are often unsuccessful in verification, compositional verification is rarely applicable. To reach the desired aim, the author follows a deductive verification approach and develops three logic formalisms and corresponding Hilbert-style sequent proof calculi for hybrid system specification and verification, all fully compositional. The first formalism introduced, Differential Dynamic Logic (dL), is an extension of dynamic logic [2] that allows hybrid programs (HP) as modalities. Hybrid programs are a novel operational model for hybrid systems, which, unlike hybrid automata, is fully compositional. The other two formalisms introduced, Differential-Algebraic Dynamic Logic (DAL) and Differential Temporal Dynamic Logic (dTL), extend dL with the aim of better handling more complex hybrid dynamics and intermediate state properties, respectively. Part I also proves a relative completeness result for each of the introduced formalisms. These are very significant results, first of their kind. In particular, differential induction, a fully algebraic technique for proving local statements about hybrid dynamics (used in the DAL logic), turns out to be extremely powerful in handling complex dynamics.
Part II deals with issues arising when automating theorem proving based on the introduced proof calculi. It shows how to handle nondeterminism arising in proofs and it presents a tableau procedure modulo background solvers. Then, it shows how to compute differential invariants (which are necessary to apply differential induction) as fixed points.
Although examples of proofs carried out through the presented proof calculi are provided throughout the book, Part III focuses solely on the application of the introduced techniques on two benchmark case studies: the European Train Control System (ETCS) and the Air Traffic Collision Avoidance (ATCA) problem. The case studies show that the deductive methods introduced in the book have a remarkable expressive power for specifying properties of interest, and they are very effective in carrying out automated proofs. One of the key strengths of these methods is that they allow for a fully automatic determination of parametric constraints, which is crucial for the targeted case studies.
Finally, the author briefly introduces a tool, named KeYmaera, that implements all presented techniques. KeYmaera is a hybrid formal verification tool for hybrid systems that combines deductive, real algebraic and computer algebraic prover technologies. It has been developed by the author on the basis of KeY [3], a semi-automated theorem prover for proving correctness properties of Java programs. KeYmaera is particularly suited for the verification of parametric hybrid systems and it has been successfully used for the analysis of collision avoidance algorithms in the railway and air transport domains. Indeed, several complex proofs are carried out in just a few seconds. KeYmaera is presented in the appendix, along with some background material (first order logic, differential equations, hybrid automata).
The book is largely self-contained: it starts with an ample introduction on the matter of study (hybrid systems and deductive approaches), then it provides the mathematical foundations of the methods presented, followed by a detailed and comprehensive description of the formalisms and related results. The exposition is clear and neat. The motivations, methods and contributions are well described. However, for reasons of brevity, existing techniques and methods are frequently used without providing a comprehensive introduction and explanation. This might hinder readers who lack a wide background on standard formal methods and on mathematical logic. In general, the level of technicality is quite high throughout the book, so even readers who have a good background in formal methods might not find it an easy read. As constructed, the book focuses on the theoretical aspects of the approach, and only at the end it presents the Keymaera tool. Hence, getting a good understanding of the features of the tool is possible only after a careful reading of the whole book; this might limit its accessibility to practitioners whose primary interests lie outside purely theoretical mathematical modeling.
All in all, the book is a very interesting read, though probably not for a wide audience. It presents a powerful formalism for hybrid systems’ specification and verification, with a strong practical impact. Nevertheless, its theory-oriented approach and its considerable level of complexity makes a keen interest in mathematical modeling a prerequisite for a thorough reading.
References
[1] A. Platzer. Logical Foundations of Cyber-Physical Systems. Springer, 2018.
[2] D. Harel. First-Order Dynamic Logic. Springer, 1979.
[3] W. Ahrendt, T. Baar, B. Beckert, R. Bubel, M. Giese, R. Haehnle, W. Menzel, W. Mostowski, A.Roth, S. Schlager, P.H. Schmitt. The KeY
Tool. Software and System Modeling 4: 32-54, 2005.