Dr. Johannes Faber
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@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. },
}
@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}}
}
@TECHREPORT{Faber2010a,
AUTHOR = {J. Faber},
TITLE = {Verification {A}rchitectures: Compositional Reasoning for Real-time
Systems},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2010},
TYPE = {Reports of SFB/TR 14 AVACS},
NUMBER = {65},
MONTH = {August},
NOTE = {ISSN: 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
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. },
ACCESS = {open},
BIBTEX = {atr065.bib},
EDITOR = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger
Olderog and Andreas Podelski and Reinhard Wilhelm},
SERIES = {ATR},
SUBPROJECT = {R1},
URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ATR065.pdf}
}
@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}
}
@TECHREPORT{FIJS2010,
AUTHOR = {Johannes Faber and Carsten Ihlemann and Swen Jacobs and Viorica Sofronie-Stokkermans},
TITLE = {Automatic Verification of Parametric Specifications with Complex
Topologies},
INSTITUTION = {SFB/TR 14 AVACS},
YEAR = {2010},
TYPE = {Reports of SFB/TR 14 AVACS},
NUMBER = {66},
NOTE = {ISSN: 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
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.},
ACCESS = {open},
BIBTEX = {atr066.bib},
EDITOR = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and Ernst-R{\"u}diger
Olderog and Andreas Podelski and Reinhard Wilhelm},
SERIES = {ATR},
SUBPROJECT = {R1},
URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ATR066.pdf},
}
@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}
}
@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},
}
@TECHREPORT{atr19,
AUTHOR = {J. Faber and I. Stierand},
TITLE = {From High-Level Verification to Real-Time Scheduling:
A Property-Preserving Integration},
EDITOR = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog and A.
Podelski and R. Wilhelm},
INSTITUTION = {SFB/TR 14 AVACS},
SUBPROJECT = {R1,R2},
YEAR = {2007},
MONTH = {June},
TYPE = {Reports of SFB/TR 14 AVACS},
SERIES = {ATR},
NUMBER = 19,
NOTE = {{ISSN} 1860-9821, \url{http://www.avacs.org}{http://www.avacs.org}.},
ABSTRACT = {
In the design process of real-time systems,
formal verification establishes global properties of high-level
specifications while real-time scheduling analysis
ensures that concrete realisations
meet essential timing properties with respect to a given target platform.
But a formal link between these phases is missing. It is unclear
(1) whether timing assumptions that are required to verify
properties of high-level specifications can actually be realised on a
target platform and (2) whether verified properties remain valid for a
schedulable task network. Our approach bridges this gap by guaranteeing that
properties verified on specification level are preserved on the implementation
level, and vice versa, schedulability results can be propagated back to the
specification.
To this end, we provide a property-preserving translation from a subclass of
the high-level real-time language CSP-OZ-DC
into Cyclic Timed Automata, a
Timed Automata based task network formalism. We apply our method
to a case study from the European Train Control System standard.
},
URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FaberStierand2007.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{MFR2006,
AUTHOR = {R. Meyer and J. Faber and A. Rybalchenko},
TITLE = {Model Checking Duration Calculus: A Practical Approach},
BOOKTITLE = {Theoretical Aspects of Computing - ICTAC 2006},
YEAR = {2006},
EDITOR = {K. Barkaoui and A. Cavalcanti and A. Cerone},
SERIES = {LNCS},
VOLUME = {4281},
PAGES = {332--346},
PDF = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/MeyerFaberRybalchenko2006.pdf},
NOTE = {This publication is available at
\url{
http://www.springerlink.com/openurl.asp?genre=article&id=doi:10.1007/11921240_23
}
{SpringerLink}},
ABSTRACT = {
Model checking of real-time systems with respect to Duration
Calculus (DC) specifications requires the translation of DC
formulae into automata-based semantics. This task is difficult to
automate. 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 real world applications. Our algorithm
significantly extends the subset of DC that can be handled. It
decomposes DC specifications into sub-properties that can be
verified independently. The decomposition bases on a novel
distributive law for DC. We implemented the algorithm as part of
our tool chain for the automated verification of systems
comprising data, communication, and real-time aspects. Our
translation facilitated a successful application of the tool chain
on an industrial case study from the European Train Control System
(ETCS).
}
}
@INPROCEEDINGS{FR06,
AUTHOR = {J. Faber and R. Meyer},
TITLE = {Model Checking Data-Dependent Real-Time Properties
of the European Train Control System},
BOOKTITLE = {Formal Methods in Computer Aided Design, 2006. FMCAD '06},
YEAR = {2006},
MONTH = NOV,
PAGES = {76--77},
PUBLISHER = {IEEE Computer Society Press},
NOTE = {This publication is available free of charge at
\url{http://doi.ieeecomputersociety.org/10.1109/FMCAD.2006.21}
{IEEE Digital Library}},
ABSTRACT = {
The behavior of embedded hardware and software systems is
determined by at least three dimensions: control flow, data
aspects, and real-time requirements. To specify the different
dimensions of a system with the best-suited techniques, the formal
language CSP-OZ-DC integrates Communicating Sequential Processes
(CSP), Object-Z (OZ), and Duration Calculus (DC) into a
declarative formalism equipped with a unified and compositional
semantics. In this paper, we provide evidence that CSP-OZ-DC is a
convenient language for modeling systems of industrial
relevance. To this end, we examine the emergency message handling
in the European Train Control System (ETCS) as a case study with
uninterpreted constants and infinite data domains. We
automatically verify that our model ensures real-time safety
properties, which crucially depend on the system?s data handling.
}
}
@INPROCEEDINGS{nwpt05,
AUTHOR = {J. Faber},
TITLE = {Verifying Real-Time aspects of the {European Train Control
System}},
BOOKTITLE = {Proceedings of the 17th Nordic Workshop on Programming Theory},
PUBLISHER = {University of Copenhagen, Denmark},
PAGES = {67--70},
YEAR = {2005},
MONTH = {October},
URL = {http://csd.informatik.uni-oldenburg.de/pub/Papers/jf05-nwpt.pdf}
}
@UNPUBLISHED{Faber2005d,
AUTHOR = {J. Faber},
TITLE = {Fault Tree Analysis with {Moby/FT}},
NOTE = {Tool presentation, Department for Computing Science, University of
Oldenburg},
YEAR = {2005},
OWNER = {jfaber},
PDF = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/ToolPresentationMobyFT.pdf}
}
