Dr. Jochen Hoenicke

 

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


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


@ARTICLE{HO02b,
  AUTHOR = {J. Hoenicke and E.-R. Olderog},
  TITLE = {{CSP-OZ-DC}: A Combination of Specification Techniques for
Processes, 
    Data and Time},
  JOURNAL = {Nordic Journal of Computing},
  YEAR = {2002},
  VOLUME = {9},
  NUMBER = {4},
  PAGES = {301--334},
  NOTE = {appeared March 2003},
  ABSTRACT = {
    CSP-OZ-DC is a new combination of three well researched formal
    techniques for the specification of processes, data and time: CSP
    [Hoa85], Object-Z [Smi00], and Duration Calculus [ZHR91]. This
    combination is illustrated by specifying the train controller of a
    case study on radio controlled railway crossings. The technical
    contribution of the paper is a smooth integration of the
    underlying semantic models and its use for verifying timing
    properties of CSP-OZ-DC specifications. This is done by combining
    the model-checkers FDR [Ros94] for CSP and UPPAAL [BLL97] for
    timed automata with a new tool \emph{f2u} that transforms FDR
    transition systems and certain patterns of Duration Calculus
    formulae into timed automata. This approach is illustrated by the
    example of a vending machine.

 \begin{thebibliography}
\bibitem{BLL97}
J.~Bengtsson, K.G. Larsen, F.~Larsson, P.~Pettersson, and Wang Yi.
\newblock Uppaal -- a tool suite for automatic verification of real-time
  systems.
\newblock In R.~Alur, T.A. Henzinger, and E.D. Sonntag, editors, {\em Hybrid
  Systems III -- Verification and Control}, volume 1066 of {\em LNCS}, pages
  232--243. Springer, 1997.

\bibitem{Hoa85}
C.A.R. Hoare.
\newblock {\em Communicating Sequential Processes}.
\newblock Prentice Hall, 1985.

\bibitem{Ros94}
A.W. Roscoe.
\newblock Model-checking {CSP}.
\newblock In A.W. Roscoe, editor, {\em A Classical Mind --- Essays in Honour of
  C.A.R.Hoare}, pages 353--378. Prentice-Hall, 1994.

\bibitem{Smi00}
G.~Smith.
\newblock {\em The Object-Z Specification Language}.
\newblock Kluwer Academic Publisher, 2000.

\bibitem{ZHR91}
C.~Zhou, C.A.R. Hoare, and A.P. Ravn.
\newblock A calculus of durations.
\newblock {\em Information Processing Letters}, 40(5):269--276, 1991.
 \end{thebibliography}
 
}
}


@INPROCEEDINGS{ho02,
  AUTHOR = {J. Hoenicke and E.-R. Olderog},
  TITLE = {{Combining Specification Techniques for Processes Data and
Time}},
  EDITOR = {M. Butler and L. Petre and K. Sere},
  BOOKTITLE = {Integrated Formal Methods},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2335},
  PUBLISHER = {Springer-Verlag},
  URL = {http://csd.Informatik.Uni-Oldenburg.DE/~skript/pub/Papers/ho02-ifm.pdf},
  YEAR = {2002},
  MONTH = {May},
  PAGES = {245--266},
  ABSTRACT = {
    We present a new combination CSP-OZ-DC of three well researched
    formal techniques for the specification of processes, data and
    time: CSP [Hoa85], Object-Z [Smi00], and Duration Calculus
    [ZHR91]. The emphasis is on a smooth integration of the underlying
    semantic models and its use for verifying properties of CSP-OZ-DC
    specifications by a combined application of the model-checkers FDR
    [Ros94] for CSP and UPPAAL [BLL97] for Timed Automata.  This
    approach is applied to part of a case study on radio controlled
    railway crossings.
  }
}


@MISC{hoe01,
  AUTHOR = {J. Hoenicke},
  TITLE = {{Specification of Radio Based Railway Crossings with the
                  Combination of CSP, OZ, and DC}},
  MONTH = JUN,
  YEAR = 2001,
  HOWPUBLISHED = {FBT 2001},
  URL = {http://www.i-u.de/fbt2001/fbt2001_docs/hoenicke.ps}
}