PEA-Toolkit - Related 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},
}


@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{HoenickeMaierFM2005,
  AUTHOR = {Jochen Hoenicke and Patrick Maier},
  TITLE = {Model-Checking of Specifications Integrating Processes, Data and
Time},
  BOOKTITLE = {FM 2005},
  EDITOR = {J.S. Fitzgerald and I.J. Hayes and A. Tarlecki},
  SERIES = {LNCS},
  VOLUME = {3582},
  PUBLISHER = {Springer},
  YEAR = {2005},
  PAGES = {465--480},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/hm05-fm.pdf},
  ABSTRACT = {
  We present a new model-checking technique for CSP-OZ-DC, a
  combination of CSP, Object-Z and Duration Calculus, that allows
  reasoning about systems exhibiting communication, data and real-time
  aspects. As intermediate layer we will use a new kind of timed
  automata that preserve events and data variables of the
  specification. These automata have a simple operational semantics
  that is amenable to verification by a constraint-based
  abstraction-refinement model checker. By means of a case study, a
  simple elevator parameterised by the number of floors, we show that
  this approach admits model-checking parameterised and infinite state
  real-time systems.
}
}


@PHDTHESIS{Hoenicke2006,
  AUTHOR = {J. Hoenicke},
  TITLE = {Combination of Processes, Data, and Time},
  SCHOOL = {University of Oldenburg},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/csp-oz-dc.pdf},
  YEAR = {2006},
  ADDRESS = {Germany}
}