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{ABOG12,
author = {K. R. Apt and F. S. de Boer and E.-R. Olderog and S. de Gouw},
title = {Verification of object-oriented programs: A transformational
approach},
journal = {J Computer System Sciences},
volume = {78},
number = {},
pages = {823--852},
year = {2012},
}
@inproceedings{Old12,
author = {E.-R. Olderog},
title = {Automatic Verification of Real-Time Systems with Rich Data -- An
Overview},
booktitle = {Theory and Applications of Models of Computation (TAMC)},
editor = {Manindra Agrawal and S. Barry Cooper and Angsheng Li},
series = {LNCS},
volume = {7287},
pages = {84--93},
publisher = {Springer},
year = {2012}
}
@article{OW12,
author = {E.-R. Olderog and R. Wilhelm},
title = {Turing und die {Verifikation}},
journal = {Informatik-Spektrum},
volume = {35},
number = {4},
pages = {271--279},
year = {2012},
}
@article{SwaminathanKatoenOlderog12,
author = {M. Swaminathan and
J.-P. Katoen and
E.-R. Olderog},
title = {Layered Reasoning for randomized distributed algorithms},
journal = {Formal Asp. Comput.},
volume = {24},
number = {4-6},
year = {2012},
pages = {477-496},
url = {http://dx.doi.org/10.1007/s00165-012-0231-x}
}
@inproceedings{straznymeyer:2012:framework,
author = {T. Strazny and R. Meyer},
title = {An Algorithmic Framework for Coverability in Well-Structured Systems},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
year = {2012},
pages = {173--182},
month = {June},
publisher = {IEEE Computer Society Conference Publishing Services},
abstract = {We generalize the backward algorithm for coverability in WSTS's to an algorithmic framework.
The idea is to consider the predecessor computation, the witness function, and the processing order as parameters.
On the theoretical side, we prove that every instantiation of the functions (that satisfies some requirements) still yields a decision procedure for coverability.
On the practical side, we show that known optimizations like partial order reduction and pruning can be formulated in our framework.
We also give a novel acceleration based instantiation.
For well-known classes of WSTS's (PN, PN+Transfer, LCS), we optimize the selection function inspired by $A^*$.
We implemented our instantiations and comment on the data structures.
Extensive experiments show that the new algorithms can compete with a state-of-the-art tool: MIST2.},
note = {Best Paper Award of ACSD}
}
@inproceedings{Lin12,
author = {S. Linker},
title = {Translating Structural Process Properties to Petri Net Markings},
booktitle = {Proceedings of the 12th International Conference on Application of Concurrency to System Design (ACSD'12)},
pages = {82--91},
publisher = {IEEE Computer Society Conference Publishing Services},
year = {2012},
month = {June},
abstract = {We introduce a spatio-temporal logic PSTL defined on Pi-Calculus processes. This logic is especially suited to formulate properties in relation to the structural semantics of the Pi-Calculus due to Meyer, a representation of processes as Petri nets. To allow for the use of well-researched verification techniques, we present a translation of a subset of PSTL to LTL on Petri nets.
We further prove soundness of our translation.}
}
@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://csd.informatik.uni-oldenburg.de/~jdq/paper/cdgl-ijcar.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/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{strazny:2011:accelerating,
author = {Tim Strazny},
title = {Accelerating Backward Reachability Analysis},
booktitle = {Proceedings of the 23rd Nordic Workshop on Programming Theory (NWPT'11)},
year = {2011},
editor = {Paul Pettersson and Cristina Seceleanu},
pages = {2--4},
month = {October},
organization = {M\"{a}lardalen University Sweden},
note = {Technical report 254/2011},
abstract = {In the context of depth-first backward reachability analysis, we identify
two general operations which allow for performance improvements,
while covering well-known techniques such as partial order methods
and pruning. We instantiate these operations with novel \emph{backward
acceleration} techniques and employ methods of \emph{guided search}
in this context. Further, we introduce \emph{support-based search
trees}, a data structure to represent upward-closed sets (ucs's)
which allows for efficient implementation of operations necessary
for the analysis.},
comment = {M\"{a}lardalen Real-Time Research Centre, Box 883, 72123 V\"{a}ster\r{a}s,
Sweden},
issn = {1404-3041}
}
@inproceedings{avacs-h3-dec-11,
author = {M. Hilscher AND S. Linker AND E.-R. Olderog AND A.P.
Ravn},
title = {An Abstract Model for Proving Safety of Multi-Lane Traffic
Manoeuvres},
booktitle = {Int'l Conf.\ on Formal Engineering Methods (ICFEM)},
year = {2011},
editor = {Shengchao Qin AND Zongyan Qiu},
volume = {6991},
series = {Lecture Notes in Computer Science},
month = {Oct.},
publisher = {Springer-Verlag},
note = {The original publication is available at \url{http://www.springerlink.com/content/y4721k1525v23520}{www.springerlink.com}.},
subproject = {H3},
pdf = {http://csd.informatik.uni-oldenburg.de/pub/Papers/hlor2011-icfem.pdf},
abstract = { We present an approach to prove safety (collision
freedom) of multi-lane motorway trac with lane-change
manoeuvres. This is ultimately a hybrid veri cation problem
due to the continuous dynamics of the cars. We abstract
from the dynamics by introducing a new spatial interval
logic based on the view of each car. To guarantee safety,
we present two variants of a lane-change controller, one
with perfect knowledge of the safety envelopes of
neighbouring cars and one which takes only the size of the
neighbouring cars into account. Based on these controllers
we provide a local safety proof for unboundedly many cars
by showing that at any moment the reserved space of each
car is disjoint from the reserved space of any other car.
}
}
@inproceedings{AVACS-H3-BRG-11,
author = {J.-D. Quesel AND M. Fr\"{a}nzle AND W. 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},
pdf = {http://csd.informatik.uni-oldenburg.de/~jdq/paper/bridging.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/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. },
}
@incollection{springerlink:10.1007/978-3-642-14600-8_40,
author = {Linker, Sven},
affiliation = {Carl von Ossietzky University of Oldenburg},
title = {Diagrammatic Specification of Mobile Real-Time Systems},
booktitle = {Diagrammatic Representation and Inference},
series = {Lecture Notes in Computer Science},
editor = {Goel, Ashok and Jamnik, Mateja and Narayanan, N.},
publisher = {Springer Berlin / Heidelberg},
isbn = {},
pages = {316-318},
volume = {6170},
url = {http://dx.doi.org/10.1007/978-3-642-14600-8_40},
note = {10.1007/978-3-642-14600-8_40},
year = {2010}
}
@inproceedings{Kem10,
author = {Stephanie Kemper},
editor = {Dave Clarke and
Gul A. Agha},
title = {Compositional Construction of Real-Time Dataflow Networks},
booktitle = {Coordination Models and Languages, 12th International Conference,
COORDINATION 2010, Amsterdam, The Netherlands, June 7-9,
2010. Proceedings},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6116},
year = {2010},
pages = {92-106},
doi = {10.1007/978-3-642-13414-2_7},
url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_COORDINATION10.pdf}
}
@book{Platzer10,
author = {Andr{\'e} Platzer},
title = {Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics},
publisher = {Springer},
address = {Heidelberg},
year = {2010},
isbn = {978-3-642-14509-4},
doi = {10.1007/978-3-642-14509-4},
url = {http://symbolaris.com/lahs/}
}
@inproceedings{HMO10,
author = {J. Hoenicke and R. Meyer and E.-R. Olderog},
title = {Kleene, Rabin, and Scott Are Available},
editor = {Paul Gastin and Fran\c{c}ois Laroussinie},
booktitle = {CONCUR 2010 - Concurrency Theory (CONCUR)},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {6269},
pages = {462-477},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-15375-4_32}
}
@article{FrJaLaSa:InfComput10,
author = {Fr\"{o}schle, Sibylle and Jan\v{c}ar, Petr and Lasota, Slawomir and Sawa, Zden\v{e}k},
title = {Non-interleaving bisimulation equivalences on Basic Parallel Processes},
journal = {Inf. Comput.},
volume = {208},
number = {1},
year = {2010},
pages = {42--62},
publisher = {Academic Press, Inc.}
}
@inproceedings{Faber2010,
author = {J. Faber},
title = {{Verification Architectures}: Compositional Reasoning for Real-time
Systems},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
series = {Lecture Notes in Computer Science},
pages = {136--151},
publisher = {Springer, Heidelberg},
doi = {10.1007/978-3-642-16265-7_11},
abstract = { We introduce a conceptual approach to decompose real-time systems,
specified by integrated formalisms: instead of showing safety of
a system directly, one proves that it is an instance of a Verification
Architecture, a safe behavioural protocol with unknowns and local
real-time assumptions. We examine how different verification techniques
can be combined in a uniform framework to reason about protocols,
assumptions, and instantiations of protocols. The protocols are specified
in CSP, extended by data and unknown processes with local assumptions
in a real-time logic. To prove desired properties, the CSP dialect
is embedded into dynamic logic and a sequent calculus is presented.
Further, we analyse the instantiation of protocols by combined specifications,
here illustrated by CSP-OZ-DC. Using an example, we show that this
approach helps us verify specifications that are too complex for
direct verification. },
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/IFM2010a.pdf},
note = {This publication is available at
\url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/978-3-642-16265-7_11}
{SpringerLink}}
}
@inproceedings{FIJ+2010,
author = {J. Faber and C. Ihlemann and S. Jacobs and V. Sofronie-Stokkermans},
title = {Automatic Verification of Parametric Specifications with Complex
Topologies},
series = {Lecture Notes in Computer Science},
booktitle = {Integrated Formal Methods},
year = {2010},
editor = {D. M{\'e}ry and S. Merz},
volume = {6396},
pages = {152--167},
publisher = {Springer, Heidelberg},
abstract = {The focus of this paper is on reducing the complexity in verification
by exploiting modularity at various levels: in specification, in
verification, and structurally. For specifications, we use the modular
language CSP-OZ-DC, which allows us to decouple verification tasks
concerning data from those concerning durations. At the verification
level, we exploit modularity in theorem proving for rich data structures
and use this for invariant checking. At the structural level, we
analyze possibilities for modular verification of systems consisting
of various components which interact. We illustrate these ideas by
automatically verifying safety properties of a case study from the
European Train Control System standard, which extends previous examples
by comprising a complex track topology with lists of track segments
and trains with different routes.},
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/IFM2010b.pdf},
note = {This publication is available at
\url{http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/978-3-642-16265-7_12}
{SpringerLink}},
doi = {http://dx.doi.org/10.1007/978-3-642-16265-7_12}
}
@inproceedings{OS10,
author = {E.-R. Olderog and M. Swaminathan},
title = {Layered Composition for Timed Automata},
editor = {K. Chatterjee and T. A Henzinger},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {6246},
publisher = {Springer-Verlag},
pages = {228-242},
year = {2010},
url = {http://dx.doi.org/10.1007/978-3-642-15297-9_18}
}
@inproceedings{MS2010,
editor = {Tayssir Touili and
Byron Cook and
Paul Jackson},
volume = {6174},
year = {2010},
pages = {175--179},
isbn = {978-3-642-14294-9},
author = {R. Meyer and T. Strazny},
title = {Petruchio: From dynamic networks to nets},
booktitle = {Proceedings of the 22nd International Conference on Computer Aided Verification 2010, CAV 2010},
series = {LNCS},
publisher = {Springer-Verlag},
abstract = {We introduce Petruchio, a tool for computing Petri net translations of dynamic networks. To cater for unbounded architectures beyond the capabilities of existing implementations, the principle fixed-point engine runs interleaved with coverability queries. We discuss algorithmic enhancements and provide experimental evidence that Petruchio copes with models of reasonable size.}
}
@inproceedings{HOP10,
author = {J. Hoenicke and E.-R. Olderog and A. Podelski},
title = {Fairness for Dynamic Control},
editor = {J. Esparza and R. Majumdar },
booktitle = {Tools and Algorithms for the Construction and Analysis of Systems (TACAS) },
series = {Lecture Notes in Computer Science},
volume = {6015},
publisher = {Springer-Verlag},
pages = {251--265},
year = {2010}
}
@inproceedings{OlPo10,
author = {E.-R. Olderog and A. Podelski},
editor = {D. Dams and U. Hannemann and M. Steffen},
title = { Explicit Fair Scheduling for Dynamic Control },
booktitle = {Concurrency, Compositionality, and Correctness },
series = {Lecture Notes in Computer Science},
volume = {5930 },
publisher = {Springer-Verlag },
pages = {96--117 },
year = {2010}
}
@article{Kem09,
author = {Stephanie Kemper},
title = {{SAT}-based {V}erification for {T}imed {C}omponent {C}onnectors},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {255},
year = {2009},
pages = {103-118},
url = {http://csd.informatik.uni-oldenburg.de/~stephie/Kemper_FOCLASA09.pdf},
doi = {10.1016/j.entcs.2009.10.027},
keywords = {Timed Constraint Automata, Abstraction Refinement, Model Checking, SAT, Component-Based Software Engineering}
}
@article{FrGo:Express09,
author = {Sibylle B. Fr{\"o}schle and
Daniele Gorla},
title = {Proceedings 16th International Workshop on Expressiveness
in Concurrency},
journal = {CoRR},
volume = {abs/0911.3189},
year = {2009}
}
@inproceedings{CzFrLa:Concur09,
author = {Czerwi\'{n}ski, Wojciech and Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {Partially-Commutative Context-Free Processes},
booktitle = {CONCUR 2009: Proceedings of the 20th International Conference on Concurrency Theory},
year = {2009},
pages = {259--273},
publisher = {Springer-Verlag}
}
@article{FrSt:ArspaWits09,
author = {Fr\"{o}schle, Sibylle and Steel, Graham},
title = {Analysing PKCS\#11 Key Management APIs with Unbounded Fresh Data},
book = {Foundations and Applications of Security Analysis: Joint Workshop on Automated Reasoning for Security Protocol Analysis and Issues in the Theory of Security, ARSPA-WITS 2009, York, UK, March 28-29, 2009, Revised Selected Papers},
year = {2009},
pages = {92--106},
publisher = {Springer-Verlag}
}
@inproceedings{Faber2009,
author = {J. Faber},
title = {Verification Architectures for Real-time Systems},
booktitle = {Proceedings of Formal Methods 2009 Doctoral Symposium},
year = {2009},
editor = {M. Mousavi and E. Sekerinski},
number = {09-15},
series = {CS-Report, Eindhoven University of Technology},
pages = {14--19},
pdf = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FM09_DS.pdf},
url = {http://alexandria.tue.nl/repository/books/654108.pdf },
institution = {Eindhoven University of Technology},
type = {CS-Report}
}
@inproceedings{ero-rm-09,
author = {E.-R. Olderog and R. Meyer},
title = {Automata-theoretic verification based on
counterexample specification},
editor = {V. Diekert and K. Weicker and N. Weicker},
booktitle = {Informatik als Dialog zwischen Theorie und Anwendung},
year = {2009},
pages = {217--225},
publisher = {Vieweg-Teubner},
}
@inproceedings{MS09,
author = {M. Fr{\"a}nzle and M. Swaminathan},
title = {Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata},
editor = {J. Ouaknine and F. Vaandrager},
booktitle = {Formal Modeling and Analysis of Timed Systems (FORMATS) },
series = {Lecture Notes in Computer Science},
volume = {5813},
publisher = {Springer-Verlag},
pages = {149-163},
year = {2009},
url = {http://dx.doi.org/10.1007/978-3-642-04368-0_13}
}
@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://symbolaris.com/pub/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://symbolaris.com/pub/etcs.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/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{sj09,
author = {Sch\"afer, A. and John, M.},
title = {Conceptional Modeling and Analysis of Spatio-Temporal Processes in
Biomolecular Systems},
booktitle = {Sixth Asia-Pacific Conference on Conceptual Modelling (APCCM 2009),
Wellington, New Zealand, January 2009},
editor = {Markus Kirchberg and Sebastian Link},
series = {CRPIT},
volume = {96},
publisher = {Australian Computer Society},
year = {2009},
pages = {39--48},
}
@article{Fr:Express08,
author = {Fr\"{o}schle, Sibylle},
title = {Adding Branching to the Strand Space Model},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {242},
number = {1},
year = {2009},
pages = {139--159},
publisher = {Elsevier Science Publishers B. V.}
}
@inproceedings{SFK08,
author = {M. Swaminathan and M. Fr{\"a}nzle and J-.P. Katoen},
title = {The Surprising Robustness of (Closed) Timed Automata against Clock-Drift},
editor = {Giorgio Ausiello and Juhani Karhum{\"a}ki},
booktitle = {IFIP International Conference on Theoretical Computer Science (IFIP TCS) },
series = {International Federation for Information Processing},
volume = {273},
publisher = {Springer},
pages = {537-553},
year = {2008},
url = {http://dx.doi.org/10.1007/978-0-387-09680-3_36}
}
@book{ABO09-Book3,
author = { K. R. Apt and F. S. de Boer and E.-R. Olderog },
title = {Verification of Sequential and Concurrent Programs,
3rd Edition},
series = {Texts in Computer Science},
publisher = {Springer-Verlag},
year = {2009},
note = {502 pp, ISBN 978-1-84882-744-8}
}
@book{OD08,
author = {E.-R. Olderog and H. Dierks},
title = {Real-Time Systems --- Formal Specification and Automatic
Verification},
publisher = {Cambridge University Press},
year = 2008,
note = {ISBN 978-0-521-88333-7. For more information see:
\url{http://csd.informatik.uni-oldenburg.de/rt-book/}{http://csd.informatik.uni-oldenburg.de/rt-book/}}
}
@inproceedings{Old08,
author = {E.-R. Olderog},
title = {Automatic Verification of Combined Specifications},
booktitle = {Proc. of the 1st Internat. Workshop on Harnessing Theories for
Tool Support in Software (TTSS 2007), Macau},
year = {2008},
editor = {G. Pu and V. Stolz},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {1571-0661},
volume = {207},
number = {},
month = {April},
pages = {3--16},
ee = {http://dx.doi.org/10.1016/j.entcs.2008.03.082},
url = {},
keywords = {Real-time systems, complex data,
CSP, Object-Z, Duration Calculus,
model checking, abstraction refinement,
UML profile, tool support},
abstract = { This paper gives an overview of results of the project
``Beyond Timed Automata'' carried out in the Collaborative Research Center AVACS
(Automatic Verification and Analysis of Complex Systems)
of the Universities of Oldenburg, Freiburg, and Saarbr\"ucken.
We discuss how properties of high-level specifications
of real-time systems combining the dimensions of
process behaviour, data, and time
can be automatically verified, exploiting recent advances
in semantics, constraint-based model checking, and
decision procedures for complex data.
As specification language we consider CS-OZ-DC,
which integrates concepts from
Communicating Sequential Processes (CSP), Object-Z (OZ),
and Duration Calculus (DC).
Our approach to automatic verification of CSP-OZ-DC rests
on a compositional semantics of this languages in terms of
Phase-Event-Automata. These can be translated into
Transition Constraint Systems which serve as an input
language of an abstract refinement model checker called
ARMC which can handle constraints covering both real-time
and infinite data.
This is demonstrated by a case study concerning emergency
messages in the European Train Control System (ETCS).
For CSP-OZ-DC we also discuss a UML profile and tool support.
}
}
@article{MORW08,
author = {M. M{\"o}ller 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 = {2008},
volume = {20},
pages = {161--204},
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.},
}
@article{schaefer2008,
author = {A. Sch\"afer},
title = {{Beschreibung und Verifikation r\"aumlicher und zeitlicher Eigenschaften
mobiler Systeme}},
journal = {it -- Information Technology},
year = {2008},
volume = {50},
pages = {324-326},
number = {5},
doi = {DOI 10.1524/itit.2008.0503},
url = {http://csd.informatik.uni-oldenburg.de/pub/Papers/itti0805_324a.pdf},
note = {\url{http://it-Information-Technology.de}{http://it-Information-Technology.de}},
abstract = {
This paper provides an overview over a formal method for the analysis of mobile real-time systems. Control systems for cars and trains as well as mobile robots are examples of such systems. We develop a spatio-temporal logic that is used to model both the systems and safety requirements. We investigate the theoretical foundations like decidability and axiomatisability and develop a prototype tool for the automatic verification based on these results. The application of this logic is exemplified with an industrial case study.}
}
@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},
doi = {10.1093/logcom/exn070},
pdf = {http://symbolaris.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://symbolaris.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, 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://symbolaris.com/pub/KeYmaera.pdf},
slides = {http://csd.informatik.uni-oldenburg.de/~jdq/slides/keymaera-slides.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://symbolaris.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}}$.}
}
@article{MeyerKhomenkoStrazny2009Unfolding,
author = {R. Meyer and V. Khomenko and T. Strazny},
title = {A Practical Approach to Verification of Mobile Systems Using Net Unfoldings},
journal = {Fundamenta Informaticae},
publisher = {IOS Press},
note = {Special Issue on Petri Nets 2008, invited version of the ATPN 2008 paper},
volume = {94},
number = {3--4},
pages = {439--471},
year = {2009},
keywords = {finite control processes, safe processes, $\pi$-Calculus, mobile
systems, model checking, Petri net unfoldings},
abstract = {
We propose a technique for verification of mobile systems. We
translate \emph{finite control processes,} which are a
well-known subset of \picalc, 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 \emph{safe processes,}
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. We also demonstrate
the applicability of our method on a realistic model of an
automated manufacturing system.}
}
@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},
pages = {327--347},
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://symbolaris.com/pub/ETCS-short.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c)
Springer-Verlag}}
}
@inproceedings{JEP08,
author = {Martin Johns and
Bj{\"o}rn Engelmann and
Joachim Posegga},
title = {XSSDS: Server-Side Detection of Cross-Site Scripting Attacks},
booktitle = {ACSAC},
year = {2008},
pages = {335-344},
abstract = {Cross-site Scripting (XSS) has emerged to one of the
most prevalent type of security vulnerabilities. While the
reason for the vulnerability primarily lies on the serverside,
the actual exploitation is within the victim's web
browser on the client-side. Therefore, an operator of a
web application has only very limited evidence of XSS issues.
In this paper, we propose a passive detection system
to identify successful XSS attacks. Based on a prototypical
implementation, we examine our approach's accuracy
and verify its detection capabilities. We compiled a data-set
of 500.000 individual HTTP request/response-pairs from 95
popular web applications for this, in combination with both
real word and manually crafted XSS-exploits; our detection
approach results in a total of zero false negatives for all
tests, while maintaining an excellent false positive rate for
more than 80\% of the examined web applications.},
bibtex = {jep08.bib},
doi = {10.1109/ACSAC.2008.36},
pdf = {http://www.acsac.org/openconf2008/modules/request.php?module=oc_proceedings&action=view.php&a=Accept&id=104}
}
@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}
}
@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://symbolaris.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://symbolaris.com/pub/dL.pdf}
}
@inproceedings{FJSS07,
author = {J. Faber and S. Jacobs and V. 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://symbolaris.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://symbolaris.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://symbolaris.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://symbolaris.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.
}
}
@article{FrLa:Infinity06,
author = {Fr\"{o}schle, Sibylle and Lasota, S\lawomir},
title = {Normed Processes, Unique Decomposition, and Complexity of Bisimulation Equivalences},
journal = {Electron. Notes Theor. Comput. Sci.},
volume = {239},
year = {2009},
pages = {17--42},
publisher = {Elsevier Science Publishers B. V.}
}
@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://symbolaris.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.
}
}