Publications (Source)

1 Publications (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.},
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. },
}

@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},
}

@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
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{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},