reviewed.bib
@inproceedings{MitschQP14,
author = {Stefan Mitsch and Jan-David Quesel and Andr{\'e} Platzer},
title = {Refactoring, Refinement, and Reasoning: A Logical Characterization for Hybrid Systems},
year = {2014},
note = {The original publication is available at \url{http://link.springer.com/chapter/10.1007/978-3-319-06410-9_33}{www.springerlink.com}.},
volume = {8442},
series = {LNCS},
pages = {481--496},
doi = {10.1007/978-3-319-06410-9_33},
editor = {Cliff B. Jones and
Pekka Pihlajasaari and
Jun Sun},
booktitle = {FM 2014: Formal Methods, 19th
International Symposium on Formal
Methods, Singapore, May 12-16, 2014,
Proceedings},
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.
},
pdf = {http://www.cs.cmu.edu/~jquesel/paper/refactoring.pdf}
}
@inproceedings{DBLP:conf/cade/QueselP12,
author = {Jan-David Quesel and Andr{\'e} Platzer},
title = {Playing Hybrid Games with {KeYmaera}.},
booktitle = {Automated Reasoning, Sixth International Joint Conference,
IJCAR 2012, Manchester, UK, Proceedings},
month = {June},
year = {2012},
editor = {Bernhard Gramlich and Dale Miller and Ulrike Sattler},
publisher = {Springer},
volume = {7364},
series = {LNCS},
pages = {439--453},
doi = {10.1007/978-3-642-31365-3_34},
pdf = {http://www.cs.cmu.edu/~jquesel/paper/cdgl-ijcar.pdf},
slides = {http://www.cs.cmu.edu/~jquesel/slides/ijcar-2012-06-26.pdf},
note = {The original publication is available at \url{http://www.springerlink.com/content/l44k5x507h67737q}{www.springerlink.com}.},
keywords = {differential dynamic logic, hybrid games, sequent calculus, theorem proving, logics for
hybrid systems, factory automation},
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.
}
}
@inproceedings{AVACS-H3-BRG-11,
author = {Jan-David Quesel AND Martin Fr\"{a}nzle AND Werner Damm},
title = {Crossing the bridge between similar games},
booktitle = {Formal Modeling and Analysis of Timed Systems - 9th International
Conference (FORMATS), Aalborg, Denmark, 21-23 September, 2011. Proceedings},
year = {2011},
editor = {Stavros Tripakis and Uli Fahrenberg},
series = {LNCS},
volume = {6919},
pages = {160--176},
month = {Sep.},
publisher = {Springer},
note = {The original publication is available at \url{http://www.springerlink.com/content/e6r94n5820k08626}{www.springerlink.com}.},
subproject = {H3},
doi = {10.1007/978-3-642-24310-3_12},
pdf = {http://www.cs.cmu.edu/~jquesel/paper/bridging.pdf},
slides = {http://www.cs.cmu.edu/~jquesel/slides/bridging-formats-2011-09-21.pdf},
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.}
}
@article{FLO+2011,
author = {Johannes Faber and Sven Linker and Ernst-R{\"u}diger Olderog and
Jan-David Quesel},
title = {Syspect - Modelling, Specifying, and Verifying Real-Time Systems with
Rich Data},
journal = {International Journal of Software and Informatics},
year = {2011},
volume = {5},
number = {1-2},
part = {1},
pages = {117--137},
note = {ISSN 1673-7288.},
url = {http://www.ijsi.org/IJSI/ch/reader/create_pdf.aspx?file_no=i78&flag=1&journal_id=ijsi},
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. },
publists = {syspect}
}
@inproceedings{DBLP:conf/cade/PlatzerQR09,
author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings},
editor = {Renate A. Schmidt},
publisher = {Springer},
volume = {5663},
pages = {485-501},
series = {LNCS},
year = {2009},
doi = {10.1007/978-3-642-02959-2_35},
pdf = {http://www.cs.cmu.edu/~jquesel/paper/rwv.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-642-02959-2_35}{(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{\"o}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{\"o}bner Bases and semidefinite programming for the real
Nullstellensatz that outperforms the individual approaches on an
interesting set of problems.}
}
@inproceedings{conf/icfem/PlatzerQ09,
author = {Andr{\'e} Platzer and Jan-David Quesel},
title = {European Train Control System: A Case Study in Formal Verification},
booktitle = {Formal Methods and Software Engineering, 11th International Conference
on Formal Engineering Methods, ICFEM 2009, Rio de Janeiro, December
9-12, 2009, Proceedings},
editor = {Ana Cavalcanti and Karin Breitman},
publisher = {Springer},
address = {Heidelberg},
series = {LNCS},
volume = {5885},
pages = {246-265},
year = {2009},
doi = {10.1007/978-3-642-10373-5_13},
pdf = {http://www.cs.cmu.edu/~jquesel/paper/etcs.pdf},
slides = {http://www.cs.cmu.edu/~jquesel/slides/ETCS-slides.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-642-10373-5_13}{(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.}
}
@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, Fourth 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},
doi = {10.1007/978-3-540-71070-7_15},
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.cs.cmu.edu/~jquesel/paper/KeYmaera.pdf},
slides = {http://www.cs.cmu.edu/~jquesel/slides/keymaera-slides.pdf}
}
@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.cs.cmu.edu/~jquesel/paper/ETCS-short.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c)
Springer-Verlag}}
}
@inproceedings{QS06,
author = {Jan-David Quesel and Andreas Sch\"afer},
title = {Spatio-Temporal Model Checking for Mobile Real-Time Systems},
booktitle = {3rd International Colloquium on Theoretical Aspects
of Computing, ICTAC},
year = {2006},
editor = {K. Barkaoui and A. Cavalcanti and A. Cerone},
series = {LNCS},
pages = {347--361},
doi = {10.1007/11921240_24},
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.
}
}