Dipl.-Inform. Johannes Faber

 

1 Publications (BibTeX Source)

@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 = {Johannes Faber and Ingo 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, 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 = {Johannes Faber and Swen Jacobs and Viorica Sofronie-Stokkermans},
  TITLE = {Verifying {CSP-OZ-DC} Specifications with Complex Data Types and
	Timing Parameters},
  BOOKTITLE = {Integrated Formal Methods},
  YEAR = {2007},
  EDITOR = {J. Davies and J. Gibbons},
  VOLUME = {4591},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {233--252},
  PUBLISHER = {Springer-Verlag},
  MONTH = JUL,
  ABSTRACT = {We extend existing verification methods for CSP-OZ-DC to
	reason about real-time systems with complex data types and timing
	parameters.
	We show that important properties of systems can be encoded
	in well-behaved logical theories in which hierarchical reasoning is
	possible.
	Thus, testing invariants and bounded model checking can be reduced
	to checking satisfiability of ground formulae over a simple base theory.
	We illustrate the ideas by means of a simplified version of a case
	study from the European Train Control System standard.},
  URL = {http://csd.informatik.uni-oldenburg.de/~jfaber/dl/FaberJacobsSofronie.pdf}
}


@INPROCEEDINGS{MFR2006,
  AUTHOR = {Roland Meyer and Johannes Faber and Andrey 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},
  URL = {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 = {Johannes Faber and Roland 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 = {Johannes 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}
}