Correct System Design
Recent Publications
On this page:
- Recent Publications (BibTeX Source)
- Publications 2004-2006
- Publications 2001-2003
- Publications 1998-2000
- Publications 1995-1997
- Publications 1991-1994
- Publications 1980-1990
back to the mainpage.
1 Recent Publications (BibTeX Source)
@ARTICLE{DBLP:journals/logcom/Platzer08, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs}, JOURNAL = {Journal of Logic and Computation}, YEAR = {2008}, NOTE = {Accepted for publication}, PDF = {http://www.functologic.com/pub/DAL.pdf}, KEYWORDS = {dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving}, ABSTRACT = { 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. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new \emph{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 a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.} } @ARTICLE{DBLP:journals/jar/Platzer08, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Differential Dynamic Logic for Hybrid Systems.}, JOURNAL = {Journal of Automated Reasoning}, YEAR = {2008}, VOLUME = {41}, NUMBER = {2}, PAGES = {143-189}, DOI = {10.1007/s10817-008-9103-8}, PDF = {http://www.functologic.com/pub/freedL.pdf}, NOTE = {\url{http://dx.doi.org/10.1007/s10817-008-9103-8}{(c) Springer-Verlag}}, KEYWORDS = {dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems}, ABSTRACT = { 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 case 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. } } @ARTICLE{Meyer2008, AUTHOR = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko}, TITLE = {Model Checking Duration Calculus: A Practical Approach}, JOURNAL = {Formal Aspects of Computing}, YEAR = {2008}, PUBLISHER = {Springer London}, VOLUME = {20}, PAGES = {481--505}, NUMBER = {4--5}, MONTH = JUL, NOTE = {{ISSN} 0934-5043 (Print) 1433-299X (Online)}, ABSTRACT = {Model checking of real-time systems against Duration Calculus (DC) specifications requires the translation of DC formulae into automata-based semantics. The existing algorithms provide a limited DC coverage and do not support compositional verification. We propose a translation algorithm that advances the applicability of model checking tools to realistic applications. Our algorithm significantly extends the subset of DC that can be checked automatically. The central part of the algorithm is the automatic decomposition of DC specifications into sub-properties that can be verified independently. The decomposition is based on a novel distributive law for DC. We implemented the algorithm in a tool chain for the automated verification of systems comprising data, communication, and real-time aspects. We applied the tool chain to verify safety properties in an industrial case study from the European Train Control System (ETCS).}, DOI = {10.1007/s00165-008-0082-7}, ISSN = {0934-5043}, KEYWORDS = {Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study}, URL = {http://www.springerlink.com/content/81g876074077601g/fulltext.pdf}, } @INPROCEEDINGS{DBLP:conf/cade/PlatzerQ08, AUTHOR = {Andr{\'e} Platzer and Jan-David Quesel}, TITLE = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.}, BOOKTITLE = {Automated Reasoning, Third International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings}, YEAR = {2008}, PAGES = {171-178}, EDITOR = {Alessandro Armando and Peter Baumgartner and Gilles Dowek}, PUBLISHER = {Springer}, SERIES = {LNCS}, VOLUME = {5195}, ISBN = {10.1007/978-3-540-71070-7_15}, ISSN = {0302-9743}, KEYWORDS = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems}, 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.}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-71070-7_15}{(c) Springer-Verlag}}, URL = {http://www.functologic.com/pub/KeYmaera.pdf} } @INPROCEEDINGS{DBLP:conf/cav/PlatzerC08, AUTHOR = {Andr{\'e} Platzer and Edmund M. Clarke}, TITLE = {Computing Differential Invariants of Hybrid Systems as Fixedpoints}, YEAR = {2008}, MONTH = {}, EDITOR = {Aarti Gupta and Sharad Malik}, BOOKTITLE = {Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings}, PUBLISHER = {Springer}, SERIES = {LNCS}, PAGES = {176-189}, VOLUME = {5123}, ISBN = {}, DOI = {10.1007/978-3-540-70545-1_17}, KEYWORDS = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine}, ABSTRACT = { We introduce a fixedpoint 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 a continuous generalization 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 fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety 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 maneuvers in air traffic management and collision avoidance in train control.}, PDF = {http://www.functologic.com/pub/fpdi.pdf}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-70545-1_17}{(c) Springer-Verlag}} } @INPROCEEDINGS{Meyer2008BoundedDepth, AUTHOR = {R. Meyer}, TITLE = {On Boundedness in Depth in the $\pi$-Calculus}, BOOKTITLE = {Proc. of the 5th IFIP International Conference on Theoretical Computer Science, IFIP TCS 2008}, SERIES = {IFIP}, VOLUME = {273}, PUBLISHER = {Springer-Verlag}, YEAR = {2008}, PAGES = {}, NOTE = {To appear}, KEYWORDS = {$\pi$-Calculus, structural congruence, well-structured transition systems, termination}, ABSTRACT = { We investigate the class $P_{\mathit{BD}}$ of $\pi$-Calculus processes that are bounded in the function depth. First, we show that boundedness in depth has an intuitive characterisation when we understand processes as graphs: a process is bounded in depth if and only if the length of the simple paths is bounded. The proof is based on a new normal form for the $\pi$-Calculus called anchored fragments. Using this concept, we then show that processes of bounded depth have well-structured transition systems (WSTS). As a consequence, the termination problem is decidable for this class of processes. The instantiation of the WSTS framework employs a new well-quasi-ordering for processes in $P_{\mathit{BD}}$.} } @INPROCEEDINGS{MeyerKhomenkoStrazny2008Unfolding, AUTHOR = {R. Meyer and V. Khomenko and T. Strazny}, TITLE = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings}, BOOKTITLE = {Proc. of the 29th International Conference on Application and Theory of Petri Nets and Other Models of Concurrency, ATPN 2008}, SERIES = {LNCS}, VOLUME = {5062}, PUBLISHER = {Springer-Verlag}, NOTE = {To appear}, YEAR = {2008}, KEYWORDS = {finite control processes, safe processes, $\pi$-Calculus, mobile systems, model checking, Petri net unfoldings}, ABSTRACT = { In this paper we propose a technique for verification of mobile systems.We translate finite control processes, which are a well-known subset of $\pi$-Calculus, into Petri nets, which are subsequently used for model checking. This translation always yields bounded Petri nets with a small bound, and we develop a technique for computing a non-trivial bound by static analysis. Moreover, we introduce the notion of safe pro- cesses, which are a subset of finite control processes, for which our translation yields safe Petri nets, and show that every finite control process can be translated into a safe one of at most quadratic size. This gives a possibility to translate every finite control process into a safe Petri net, for which efficient unfolding-based verification is possible. Our experiments show that this approach has a significant advantage over other existing tools for verification of mobile systems in terms of memory consumption and runtime.} } @INPROCEEDINGS{DBLP:conf/hybrid/PlatzerQ08, AUTHOR = {Andr{\'e} Platzer and Jan-David Quesel}, TITLE = {Logical Verification and Systematic Parametric Analysis in Train Control.}, YEAR = {2008}, PAGES = {646-649}, DOI = {10.1007/978-3-540-78929-1_55}, EDITOR = {Magnus Egerstedt and Bud Mishra}, BOOKTITLE = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2008, St. Louis, USA, Proceedings}, PUBLISHER = {Springer}, SERIES = {LNCS}, VOLUME = {4981}, ISBN = {}, KEYWORDS = {parametric verification, logic for hybrid systems, symbolic decomposition}, 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.}, URL = {http://www.functologic.com/pub/ETCS-short.pdf}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c) Springer-Verlag}} } @INPROCEEDINGS{Meyer2007Dagstuhl, AUTHOR = {R. Meyer}, TITLE = {{A Petri Net Semantics for $\pi$-Calculus Verification}}, BOOKTITLE = {Dagstuhl ''zehn plus eins''}, PAGES = {76--77}, YEAR = {2007}, PUBLISHER = {Verlagshaus Mainz GmbH Aachen}, } @ARTICLE{FrLa:TCS07, AUTHOR = {Sibylle Fr{\"o}schle and S{\l}awomir Lasota}, TITLE = {Causality versus true-concurrency}, JOURNAL = {Theoretical Computer Science}, YEAR = {2007}, VOLUME = {386}, NUMBER = {3}, PAGES = {169--187}, } @ARTICLE{AVACS07, AUTHOR = {B. Becker and A. Podelski and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and R. Wilhelm}, TITLE = {{SFB/TR 14 AVACS -- Automatic Verification and Analysis of Complex Systems}}, JOURNAL = {it -- Information Technology}, PUBLISHER = {Oldenbourg}, YEAR = {2007}, NUMBER = {2}, VOLUME = {49}, PAGES = {118--126}, NOTE = {See also \url{http://www.avacs.org}{http://www.avacs.org}} } @ARTICLE{sch07b, AUTHOR = {A. Sch\"afer}, TITLE = {{PhD Abstract: Specification and Verification of Mobile Real-Time Systems}}, EDITOR = {V. Sassone}, YEAR = {2007}, PAGES = {193-195}, PUBLISHER = {EATCS}, JOURNAL = {Bulletin of the EATCS}, VOLUME = {92}, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07b.pdf} } @INPROCEEDINGS{sch07a, AUTHOR = {A. Sch\"afer}, TITLE = {{Spezifikation und Verifikation mobiler Realzeitsysteme}}, BOOKTITLE = {{Ausgezeichnete Informatikdissertationen 2007}}, EDITOR = {D. Wagner}, YEAR = {2007}, PAGES = {169-177}, SERIES = {GI-Edition-Lecture Notes in Informatics (LNI)}, PUBLISHER = {Gesellschaft f\"ur Informatik}, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/as07a.pdf} } @ARTICLE{MORW07, AUTHOR = {M. M\"oller and E.-R. Olderog and H. Rasch and H. Wehrheim}, TITLE = {Integrating a Formal Method into a Software Engineering Process with {UML} and {Java}}, JOURNAL = {Formal Apsects of Computing}, YEAR = {2007}, VOLUME = {}, NUMBER = {}, NOTE = {To appear.}, ABSTRACT = { We describe how CSP-OZ, a formal method combining the process algebra CSP with the specification language Object-Z, can be integrated into an object-oriented software engineering process employing the UML as a modelling and Java as an implementation language. The benefit of this integration lies in the rigour of the formal method, which improves the precision of the constructed models and opens up the possibility of (1) verifying properties of models in the early design phases, and (2) checking adherence of implementations to models. The envisaged application area of our approach is the design of distributed {\em reactive systems}. To this end, we propose a specific UML {\em profile} for reactive systems. The profile contains facilities for modelling components, their interfaces and interconnections via synchronous/broadcast communication, and the overall architecture of a system. The integration with the formal method proceeds by generating a significant part of the CSP-OZ specification from the initially developed UML model. The formal specification is on the one hand the starting point for {\em verifying} properties of the model, for instance by using the FDR model checker. On the other hand, it is the basis for generating {\em contracts} for the final implementation. Contracts are written in the Java Modeling Language (JML) complemented by \CSPjassda{}, an assertion language for specifying orderings between method invocations. A set of tools for runtime checking can be used to supervise the adherence of the final Java implementation to the generated contracts. } } @INPROCEEDINGS{DBLP:conf/verify/Platzer07, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Combining Deduction and Algebraic Constraints for Hybrid System Analysis.}, BOOKTITLE = {4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany}, YEAR = {2007}, PAGES = {164-178}, EDITOR = {Bernhard Beckert}, VOLUME = {259}, PUBLISHER = {CEUR-WS.org}, SERIES = {}, NOTE = {\url{http://ceur-ws.org/Vol-259}{CEUR Workshop Proceedings}}, ISSN = {1613-0073}, KEYWORDS = {modular prover combination, analytic tableaux, verification of hybrid systems, dynamic logic}, ABSTRACT = { We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. 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. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.}, URL = {http://www.functologic.com/pub/cdachsa.pdf} } @INPROCEEDINGS{DammMOOPPSW07, AUTHOR = {Werner Damm and Alfred Mikschl and Jens Oehlerking and Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc Segelken and Boris Wirtz}, TITLE = {Automating Verification of Cooperation, Control, and Design in Traffic Applications.}, YEAR = {2007}, PAGES = {115--169}, EDITOR = {Cliff Jones and Zhiming Liu and Jim Woodcock}, BOOKTITLE = {Formal Methods and Hybrid Real-Time Systems}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, VOLUME = {4700}, DOI = {10.1007/978-3-540-75221-9_6}, ISSN = {}, KEYWORDS = {}, ABSTRACT = { We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-75221-9_6}{(c) Springer-Verlag}} } @INPROCEEDINGS{BSO07, AUTHOR = {D. Basin and E.-R. Olderog and P.E. Sevin\c{c}}, TITLE = {Specifying and analyzing security automata using {CSP-OZ}}, BOOKTITLE = {Proceedings of the 2007 ACM Symposium on Information, Computer and Communications Security (ASIACCS 2007)}, PAGES = {70--81}, YEAR = 2007, MONTH = {March}, PUBLISHER = {ACM Press}, LOCATION = {Singapore}, ABSTRACT = { Security automata are a variant of B\"uchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) and Object-Z (OZ), to specify security automata, formalize their combination with target systems, and analyze the security of the resulting system specifications. We provide theoretical results relating CSP-OZ specifications and security automata and show how refinement can be used to reason about specifications of security automata and their combination with target systems. Through a case study, we provide evidence for the practical usefulness of this approach. This includes the ability to specify concisely complex operations and complex control, support for structured specifications, refinement, and transformational design, as well as automated, tool-supported analysis. } } @INPROCEEDINGS{Froeschle:CSF07, AUTHOR = {Sibylle Fr{\"o}schle}, TITLE = {The Insecurity Problem: tackling Unbounded Data}, BOOKTITLE = {IEEE Computer Security Foundations Symposium 2007}, YEAR = {2007}, PUBLISHER = {IEEE Computer Society}, ABSTRACT = { In this paper we focus on tackling the insecurity problem of security protocols in the presence of an unbounded number of data such as nonces or session keys. First, we pinpoint four open problems in this category. The first two problems concern protocols with natural restrictions that any `realistic' protocol should satisfy while the second two concern protocols with disequality constraints. For protocols with disequality constraints we will prove: (1)~Insecurity is decidable in NEXPTIME when bounding the size of messages and not requiring data to be \emph{freshly} generated. (2)~Insecurity is NEXPTIME-complete when bounding the size of messages and the number of freshly generated data used in honest sessions. This shows that unbounded data can be tackled in settings which do not trivially reduce to the case of bounded data. The second result is in contrast with a recently published proof, which appears to prove the same problem undecidable. We will point out why this proof cannot be considered to be valid. }, } @INPROCEEDINGS{DBLP:conf/tableaux/Platzer07, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Differential Dynamic Logic for Verifying Parametric Hybrid Systems.}, PAGES = {216-232}, DOI = {10.1007/978-3-540-73099-6_17}, KEYWORDS = {dynamic logic, sequent calculus, verification of parametric hybrid systems, quantifier elimination}, ABSTRACT = { We introduce a first-order dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and first-order definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.}, BOOKTITLE = {Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings}, YEAR = {2007}, EDITOR = {Nicola Olivetti}, VOLUME = {4548}, SERIES = {LNCS}, PUBLISHER = {Springer-Verlag}, ISBN = {}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-73099-6_17}{(c) Springer-Verlag}}, URL = {http://www.functologic.com/pub/dL.pdf} } @INPROCEEDINGS{FJSS07, AUTHOR = {Johannes Faber and Swen Jacobs and Viorica Sofronie-Stokkermans}, TITLE = {Verifying {CSP-OZ-DC} Specifications with Complex Data Types and Timing Parameters}, BOOKTITLE = {Integrated Formal Methods}, YEAR = {2007}, EDITOR = {J. Davies and J. Gibbons}, VOLUME = {4591}, SERIES = {Lecture Notes in Computer Science}, PAGES = {233--252}, PUBLISHER = {Springer-Verlag}, MONTH = JUL, ABSTRACT = {We extend existing verification methods for CSP-OZ-DC to reason about real-time systems with complex data types and timing parameters. We show that important properties of systems can be encoded in well-behaved logical theories in which hierarchical reasoning is possible. Thus, testing invariants and bounded model checking can be reduced to checking satisfiability of ground formulae over a simple base theory. We illustrate the ideas by means of a simplified version of a case study from the European Train Control System standard.}, URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FaberJacobsSofronie.pdf} } @INPROCEEDINGS{ib07ifm, AUTHOR = {I. Br{\"u}ckner}, TITLE = {{Slicing Concurrent Real-Time System Specifications for Verification}}, BOOKTITLE = {Integrated Formal Methods}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {4591}, PUBLISHER = {Springer-Verlag}, ISSN = {0302-9743}, ISBN = {978-3-540-73209-9}, EDITOR = {J. Davies and J. Gibbons}, PAGES = {54--74}, MONTH = JUL, YEAR = {2007}, ABSTRACT = { The high-level specification language CSP-OZ-DC has been shown to be well-suited for modelling and analysing industrially relevant concurrent real-time systems. It allows to model each of the most important functional aspects such as control flow, data, and real-time requirements in adequate notations, maintaining a common semantical foundation for subsequent verification. Slicing on the other hand has become an established technique to complement the fight against state space explosion during verification which inherently accompanies increasing system complexity. In this paper, we exploit the special structure of CSP-OZ-DC specifications by extending the dependence graph---which usually serves as a basis for slicing---with several new types of dependencies, including timing dependencies derived from the specification's DC part. Based on this we show how to compute a specification slice and prove correctness of our approach. }, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07ifm.pdf} } @INPROCEEDINGS{BDFW07, AUTHOR = {I. Br\"uckner and K. Dr\"ager and B. Finkbeiner and H. Wehrheim}, TITLE = {{Slicing Abstractions}}, BOOKTITLE = {FSEN 2007: IPM International Symposium on Fundamentals of Software Engineering}, SERIES = {Lecture Notes in Computer Science}, VOLUME = {4767}, PUBLISHER = {Springer}, ISSN = {}, ISBN = {978-3-540-75697-2}, EDITOR = {F. Arbab and M. Sirjani}, PAGES = {17--32}, MONTH = {April}, YEAR = {2007}, ABSTRACT = { Abstraction and slicing are both techniques for reducing the size of the state space to be inspected during verification. In this paper, we present a new model checking procedure for infinite-state concurrent systems that interleaves automatic abstraction refinement, which splits states according to new predicates obtained by Craig interpolation, with slicing, which removes irrelevant states and transitions from the abstraction. The effects of abstraction and slicing complement each other. As the refinement progresses, the increasing accuracy of the abstract model allows for a more precise slice; the resulting smaller representation gives room for additional predicates in the abstraction. The procedure terminates when an error path in the abstraction can be concretized, which proves that the system is erroneous, or when the slice becomes empty, which proves that the system is correct. }, URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/ib07fsen.pdf} } @INPROCEEDINGS{DBLP:conf/lfcs/Platzer07, AUTHOR = {Andr{\'e} Platzer}, TITLE = {A Temporal Dynamic Logic for Verifying Hybrid System Invariants.}, EDITOR = {S. Artemov and A. Nerode}, DOI = {10.1007/978-3-540-72734-7_32}, BOOKTITLE = {Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings}, PUBLISHER = {Springer}, SERIES = {LNCS}, YEAR = {2007}, PAGES = {457--471}, VOLUME = {4514}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-72734-7_32}{(c) Springer-Verlag}}, URL = {http://www.functologic.com/pub/dTL.pdf}, KEYWORDS = {dynamic logic, sequent calculus, logic for hybrid systems, temporal logic, deductive verification of embedded systems}, ABSTRACT = { We combine first-order dynamic logic for reasoning about 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 dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to non-temporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints. } } @INPROCEEDINGS{DBLP:conf/hybrid/Platzer07, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Differential Logic for Reasoning about Hybrid Systems.}, YEAR = {2007}, EDITOR = {A. Bemporad and A. Bicchi and G. Buttazzo}, BOOKTITLE = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, PAGES = {746--749}, DOI = {10.1007/978-3-540-71493-4_75}, VOLUME = {4416}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_75}{(c) Springer-Verlag}}, URL = {http://www.functologic.com/pub/dL-short.pdf}, KEYWORDS = {dynamic logic, hybrid systems, parametric verification}, ABSTRACT = { We propose a first-order dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using first-order variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components. } } @INPROCEEDINGS{DBLP:conf/hybrid/PlatzerC07, AUTHOR = {Andr{\'e} Platzer and Edmund M. Clarke}, TITLE = {The Image Computation Problem in Hybrid Systems Model Checking.}, YEAR = {2007}, DOI = {10.1007/978-3-540-71493-4_37}, EDITOR = {A. Bemporad and A. Bicchi and G. Buttazzo}, BOOKTITLE = {Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings}, PUBLISHER = {Springer-Verlag}, SERIES = {LNCS}, PAGES = {473--486}, VOLUME = {4416}, KEYWORDS = {model checking, hybrid systems, image computation}, NOTE = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_37}{(c) Springer-Verlag}}, URL = {http://www.functologic.com/pub/happroximation.pdf}, ABSTRACT = { In this paper, we analyze limits of approximation techniques for (non-linear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance. } } @ARTICLE{schaefer07, AUTHOR = {A. Sch\"afer}, TITLE = {Axiomatisation and Decidability of Multi-Dimensional Duration Calculus}, JOURNAL = {TIME'05 special issue of Information and Computation}, YEAR = {2007}, VOLUME = {205}, NUMBER = {1}, NOTE = {DOI \url{http://dx.doi.org/10.1016/j.ic.2006.08.005}{10.1016/j.ic.2006.08.005} }, ABSTRACT = { The Shape Calculus is a spatio-temporal logic based on an $n$-dimensional Duration Calculus tailored for the specification and verification of mobile real-time systems. After showing non-axiomatisability, we give a complete embedding in $n$-dimensional interval temporal logic and present two different decidable subsets, which are important for tool support and practical use. } } @INPROCEEDINGS{DBLP:journals/entcs/KemperP07, AUTHOR = {Stephanie Kemper and Andr{\'e} Platzer}, TITLE = {SAT-based Abstraction Refinement for Real-time Systems}, BOOKTITLE = {Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings}, YEAR = {2007}, EDITOR = {Frank S. de Boer and Vladimir Mencl}, JOURNAL = {Electr. Notes Theor. Comput. Sci.}, VOLUME = {182}, SERIES = {ENTCS}, ISSN = {1571-0661}, PAGES = {107-122}, DOI = {10.1016/j.entcs.2006.09.034}, URL = {http://www.functologic.com/pub/SAAtRe.pdf}, KEYWORDS = {abstraction refinement, model checking, real-time systems, SAT, Craig interpolation}, ABSTRACT = { In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. With a faithful embedding of bounded model checking for systems of timed automata into propositional logic and linear arithmetic, we achieve both, quick abstraction techniques and a linear-size representation of parallel composition. In this logical setting, we introduce an abstraction that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement. } } @INPROCEEDINGS{DBLP:journals/entcs/Platzer07, AUTHOR = {Andr{\'e} Platzer}, TITLE = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems}, BOOKTITLE = {Proc., LICS International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA}, YEAR = {2007}, EDITOR = {Patrick Blackburn and Thomas Bolander and Torben Bra\"{u}ner and Valeria de Paiva and J{\o}rgen Villadsen}, SERIES = {ENTCS}, JOURNAL = {Electr. Notes Theor. Comput. Sci.}, ISSN = {1571-0661}, VOLUME = {174}, NUMBER = {6}, MONTH = {Jun}, PAGES = {63-77}, DOI = {10.1016/j.entcs.2006.11.026}, URL = {http://www.functologic.com/pub/hdL.pdf}, KEYWORDS = {hybrid logic, dynamic logic, sequent calculus, compositional verification, real-time hybrid dynamic systems}, ABSTRACT = { We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces state-based reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic advances the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goal-oriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus. } }