Peer-Reviewed Publications

[MQP14] Stefan Mitsch, Jan-David Quesel, and André Platzer. Refactoring, refinement, and reasoning: A logical characterization for hybrid systems. In Cliff B. Jones, Pekka Pihlajasaari, and Jun Sun, editors, FM 2014: Formal Methods, 19th International Symposium on Formal Methods, Singapore, May 12-16, 2014, Proceedings, volume 8442 of LNCS, pages 481-496, 2014. The original publication is available at www.springerlink.com.
Abstract
Refactoring of code is a common device in classical programs. As cyber-physical systems (CPS) become ever more complex, similar engineering practices become more common in CPS development. Proper safe developments of CPS designs are accompanied by a proof of correctness. Since the inherent complexities of CPS practically mandate iterative development, frequent changes of models are standard practice, but require reverification of the resulting models after every change.

To overcome this issue, we develop proof-aware refactorings for CPS. That is, we study model transformations on CPS and show how they correspond to relations on correctness proofs. As the main technical device, we show how the impact of model transformations on correctness can be characterized by different notions of refinement in differential dynamic logic. Furthermore, we demonstrate the application of refinements on a series of safety-preserving and liveness preserving refactorings. For some of these we can give strong results by proving on a meta-level that they are correct. Where this is impossible, we construct proof obligations for showing that the refactoring respects the refinement relation.

[QP12] Jan-David Quesel and André Platzer. Playing hybrid games with KeYmaera. In Bernhard Gramlich, Dale Miller, and Ulrike Sattler, editors, Automated Reasoning, Sixth International Joint Conference, IJCAR 2012, Manchester, UK, Proceedings, volume 7364 of LNCS, pages 439-453. Springer, June 2012. The original publication is available at www.springerlink.com.
Abstract
We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario.

[QFD11] Jan-David Quesel, Martin Fränzle, and Werner Damm. Crossing the bridge between similar games. In Stavros Tripakis and Uli Fahrenberg, editors, Formal Modeling and Analysis of Timed Systems - 9th International Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings, volume 6919 of LNCS, pages 160-176. Springer, Sep. 2011. The original publication is available at www.springerlink.com.
Abstract
Specifications and implementations of complex physical systems tend to differ as low level effects such as sampling are often ignored when high level models are created. Thus, the low level models are often not exact refinements of the high level specification. However, they are similar to those. To bridge the gap between those models, we study robust simulation relations for hybrid systems. We identify a family of robust simulation relations that allow for certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of simulation a broad class of logical properties is preserved. The question whether two systems are in simulation relation can be reduced to a reach avoid problem for hybrid games. We provide a sufficient condition under which a winning strategy for these games exists.

[FLOQ11] Johannes Faber, Sven Linker, Ernst-Rüdiger Olderog, and Jan-David Quesel. Syspect - modelling, specifying, and verifying real-time systems with rich data. International Journal of Software and Informatics, 5(1-2):117-137, 2011. ISSN 1673-7288.
Abstract
We introduce the graphical tool Syspect for modelling, specifying, and automatically verifying reactive systems with continuous real-time constraints and complex, possibly infinite data. For modelling these systems, a UML profile comprising component diagrams, protocol state machines, and class diagrams is used; for specifying the formal semantics of these models, the combination CSP-OZ-DC of CSP (Communicating Sequential Processes), OZ (Object-Z) and DC (Duration Calculus) is employed; for verifying properties of these specifications, translators are provided to the input formats of the model checkers ARMC (Abstraction Refinement Model Checker) and SLAB (Slicing Abstraction model checker) as well as the tool H-PILoT (Hierarchical Proving by Instantiation in Local Theory extensions). The application of the tool is illustrated by a selection of examples that have been successfully analysed with Syspect.

[PQR09] André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. In Renate A. Schmidt, editor, Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. (c) Springer-Verlag.
Abstract
Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.

[PQ09] André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. In Ana Cavalcanti and Karin Breitman, editors, Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December 9-12, 2009, Proceedings, volume 5885 of LNCS, pages 246-265, Heidelberg, 2009. Springer. (c) Springer-Verlag.
Abstract
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 its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we 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. Finally we verify that safety is preserved when a PI controller is used for speed supervision.

[PQ08a] André Platzer and Jan-David Quesel. KeYmaera: A hybrid theorem prover for hybrid systems. In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pages 171-178. Springer, 2008. (c) Springer-Verlag.
Abstract
KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.

[PQ08b] André Platzer and Jan-David Quesel. Logical verification and systematic parametric analysis in train control. In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pages 646-649. Springer, 2008. (c) Springer-Verlag.
Abstract
We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logic-based decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.

[QS06] Jan-David Quesel and Andreas Schäfer. Spatio-temporal model checking for mobile real-time systems. In K. Barkaoui, A. Cavalcanti, and A. Cerone, editors, 3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, LNCS, pages 347-361, 2006.
Abstract
This paper presents an automatic verification method for combined temporal and spatial properties of mobile real-time systems. To this end, we provide a translation of the Shape Calculus (SC), a spatio-temporal extension of Duration Calculus, into weak second order logic of one successor (WS1S). A prototypical implementation facilitates successful verification of spatio-temporal properties by translating SC specifications into the syntax of the WS1S checker MONA. For demonstrating the formalism and tool usage, we apply it to the benchmark case study “generalised railroad crossing” (GRC) enriched by requirements inexpressible in non-spatial formalisms.

Theses

[JDQ13] Jan-David Quesel. Similarity, Logic, and Games - Bridging Modeling Layers of Hybrid Systems. PhD thesis, University of Oldenburg, 2013.
Abstract
Specifications and implementations of complex physical systems tend to differ as low-level effects such as sampling are often ignored when high-level models are created. Thus, the low-level models are often not exact refinements of the high-level specification. However, intuitively we would consider them as similar. To bridge the gap between these models, we study notions of similarity and robust refinement relations for hybrid systems. We identify a family of such relations which permit certain bounded deviations in the behavior of a system specification and its implementation in both values of the system variables and timings. We show that for this relaxed version of refinement a broad class of properties is preserved. This includes stability, safety, as well as bounded response properties. The question whether two systems are in refinement relation can be reduced to a reachability problem for hybrid games.
For the study of parametric hybrid games, we propose a new logic, called differential dynamic game logic (dDGL), and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic (dL). Subsequently, we provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. Furthermore, we have implemented dDGL in our theorem prover KeYmaera. We demonstrate the strength of dDGL by applying KeYmaera to a case study in which a robot plays a game against other agents in a factory automation scenario.
KeYmaera is a theorem prover for hybrid system verification. It reduces the verification task to smaller subtasks that can be decided by quantifier elimination. Unfortunately, quantifier elimination over the reals is doubly exponential in the number of quantifier alternations already in theory and even in the number of variables in many implementations. Therefore, we compare different implementations of procedures for quantifier elimination and alternative methods for dealing with these subtasks.
We show that our dDGL-based approach for proving that two hybrid systems are in robust refinement relation can be effectively used. For this, we present a case study from the domain of train control with a safe specification using instantaneous and imperfect implementations which suffer from communication delays.

[JDQ07] Jan-David Quesel. A Theorem Prover for Differential Dynamic Logic: Deductive Verification of Hybrid Systems. Master's thesis, University of Oldenburg, 2007.
Abstract
This thesis aims at the computer aided verification of hybrid systems using deductive techniques. We have developed an interactive verification tool on the basis of a sound sequent calculus for dL. The logic dL is a dynamic logic with a special focus on the specification and verification of hybrid systems. Our implementation extends the theorem prover component of the KeY system with rules and data structures for handling dL formulas. Additionally, we have integrated KeY with the computer algebra system Mathematica to handle quantifiers over the reals and real arithmetic. In order to demonstrate that our implementation can be used for verifying larger systems, we prove safety in a case study from the context of the European Train Control System (ETCS).

[JDQ05] Jan-David Quesel. MoDiShCa - Model Checking Discrete Shape Calculus, 2005.
Abstract
This thesis describes how a decidable fragment of the Shape Calculus, an extended Duration Calculus, can be translated into WS1S. WS1S is the monadic second order logic with one successor. We generalise a translation for the two dimensional case to an arbitrary number of dimensions and beyond an implementation of it will be presented: MoDiShCa. Also we will illustrate how this tool can be used to verify complex systems by presenting a case study.

Technical Reports

[QP12] Jan-David Quesel and André Platzer. Playing hybrid games with KeYmaera. Reports of SFB/TR 14 AVACS 84, SFB/TR 14 AVACS, April 2012. ISSN: 1860-9821, http://www.avacs.org.
Abstract
We propose a new logic, called differential dynamic game logic (dDGL), for expressing properties of parametric hybrid games, and develop a theorem prover for it. We give an operational and a modal semantics of dDGL and prove their equivalence. To allow for deductive reasoning, we exploit the fact that dDGL is a conservative extension of differential dynamic logic(dL). We provide rules for extending the dL sequent proof calculus to handle the dDGL specifics. We have implemented dDGL in the theorem prover KeYmaera and consider a case study in which a robot plays a game against other agents in a factory automation scenario.

[PQR09] André Platzer, Jan-David Quesel, and Philipp Rümmer. Real world verification. Reports of SFB/TR 14 AVACS 52, SFB/TR 14 AVACS, June 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract
Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of real-world applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of real-closed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.

[PQ09] André Platzer and Jan-David Quesel. European train control system: A case study in formal verification. Reports of SFB/TR 14 AVACS 54, SFB/TR 14 AVACS, Oct 2009. ISSN: 1860-9821, http://www.avacs.org.
Abstract
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 its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we 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. Finally we verify that safety is preserved when a PI controller is used for speed supervision.