Dr. Jochen Hoenicke

 

1 Publications (with abstracts)

[MFHR08]

R. Meyer, J. Faber, J. Hoenicke, and A. Rybalchenko. Model checking duration calculus: A practical approach. Formal Aspects of Computing, 20(4-5):481-505, July 2008. ISSN 0934-5043 (Print) 1433-299X (Online).
[ bib | .pdf ]

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).

Keywords: Model checking, Verification, Duration Calculus, Timed automata, Real-time systems, European Train Control System, Case study

[HM05]

Jochen Hoenicke and Patrick Maier. Model-checking of specifications integrating processes, data and time. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, FM 2005, volume 3582 of LNCS, pages 465-480. Springer, 2005.
[ bib | .pdf ]

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.

[HO02b]

J. Hoenicke and E.-R. Olderog. CSP-OZ-DC: A combination of specification techniques for processes, data and time. Nordic Journal of Computing, 9(4):301-334, 2002. appeared March 2003.
[ bib ]

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

References

[BLL97]

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

[Hoa85]

C.A.R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[Ros94]

A.W. Roscoe. Model-checking CSP. In A.W. Roscoe, editor, A Classical Mind - Essays in Honour of C.A.R.Hoare, pages 353-378. Prentice-Hall, 1994.

[Smi00]

G. Smith. The Object-Z Specification Language. Kluwer Academic Publisher, 2000.

[ZHR91]

C. Zhou, C.A.R. Hoare, and A.P. Ravn. A calculus of durations. Information Processing Letters, 40(5):269-276, 1991.

[HO02a]

J. Hoenicke and E.-R. Olderog. Combining Specification Techniques for Processes Data and Time. In M. Butler, L. Petre, and K. Sere, editors, Integrated Formal Methods, volume 2335 of Lecture Notes in Computer Science, pages 245-266. Springer-Verlag, May 2002.
[ bib | .pdf ]

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.

[Hoe01]

J. Hoenicke. Specification of Radio Based Railway Crossings with the Combination of CSP, OZ, and DC. FBT 2001, June 2001.
[ bib | .ps ]