Publications

[PH12]: Amalinda Post and Jochen Hoenicke. Formalization and analysis of real-time requirements: a feasibility study at BOSCH. In VSTTE 12, LNCS. Springer, 2012. To appear. [ bib ]
In this paper, we evaluate a tool chain to algorithmically analyze real-time requirements. According to this tool chain, one formalizes the requirements in a natural-language pattern system. The requirements can then be automatically compiled into formulas in a real-time logic. The formulas can be checked automatically for properties whose violation indicates an error in the requirements specification (the properties considered are: consistency, rt-consistency, vacuity). We report on a feasibility study in the context of several automotive projects at Bosch. The results of the study indicate that the effort for the formalization of real-time requirements is acceptable; the analysis algorithms are computationally feasible; the benefit (the detection of specification errors resp. the formal guarantee of their absence) seems significant.
[EHP12]: Evren Ermis, Jochen Hoenicke, and Andreas Podelski. Splitting via interpolants. In VMCAI 12, LNCS. Springer, 2012. To appear. [ bib ]
A common problem in software model checking is the automatic computation of accurate loop invariants. Loop invariants can be derived from interpolants for every path leading through the corresponding loop header. However, in practice, the consideration of single paths often leads to very path specific interpolants. Inductive invariants can only be derived after several iterations by also taking previous interpolants into account. In this paper, we introduce a software model checking approach that uses the concept of path insensitive interpolation to compute loop invariants. In contrast to current approaches, path insensitive interpolation summarizes several paths through a program location instead of one. As a consequence, it takes the abstraction refinement considerably less effort to obtain an adequate interpolant. First experiments show the potential of our approach.
[PHP11b]: Amalinda Post, Jochen Hoenicke, and Andreas Podelski. Vacuous real-time requirements. In RE 11, pages 153-162. IEEE, 2011. [ bib | DOI ]
We introduce the property of vacuity for requirements. A requirement is vacuous in a set of requirements if it is equivalent to a simpler requirement in the context of the other requirements. For example, the requirement “if A then B” is vacuous together with the requirement “not A”. The existence of a vacuous requirement is likely to indicate an error. We give an algorithm that proves the absence of this kind of error for real-time requirements. A case study in an industrial context demonstrates the practical potential of the algorithm.
[PHP11a]: Amalinda Post, Jochen Hoenicke, and Andreas Podelski. rt-inconsistency: a new property for real-time requirements. In FASE 2011, number 6603 in LNCS, pages 34-49. Springer, 2011. [ bib | DOI ]
We introduce rt-inconsistency, a property of real-time requirements. The property reflects that the requirements specify apparently inconsistent timing constraints. We present an algorithm to check rt-inconsistency automatically. The algorithm works via a stepwise reduction to real-time model checking. We implement the algorithm using an existing module for the reduction and the UPPAAL tool for the realtime model checking. As a case study, we apply our prototype implementation to existing real-time requirements for automotive projects at Bosch. The case study demonstrates the relevance of rt-inconsistency for detecting errors in industrial real-time requirements specifications.
[HLP⁺10]: J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies. Doomed program points. Formal Methods in System Design, 37(2-3):171-199, December 2010. [ bib | DOI ]
Any programming error that can be revealed before compiling a program saves precious time for the programmer. While integrated development environments already do a good job by detecting, e.g., data-flow abnormalities, current static analysis tools suffer from false positives ("noise") or require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if its execution will inevitably fail, regardless of which state it is started in. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on experiments with a prototype tool.
[HMO10]: J. Hoenicke, R. Meyer, and E.-R. Olderog. Kleene, Rabin, and Scott are available. In CONCUR 2010, number 6269 in LNCS, pages 462-477. Springer, 2010. [ bib | DOI ]
We are concerned with the availability of systems, defined as the ratio between time of correct functioning and uptime. We propose to model guaranteed availability in terms of regular availability expressions (rae) and availability automata. We prove that the intersection problem of rae is undecidable. We establish a Kleene theorem that shows the equivalence of the formalisms and states precise correspondence of flat rae and simple availability automata. For these automata, we provide an extension of the powerset construction for finite automata due to Rabin and Scott. As a consequence, we can state a complementation algorithm. This enables us to solve the synthesis problem and to reduce model checking of availability properties to reachability.
[HOP10]: J. Hoenicke, E.-R. Olderog, and A. Podelski. Fairness for dynamic control. In TACAS 2010, number 6015 in LNCS, pages 251-265. Springer, 2010. [ bib | DOI ]
Already in Lamport's bakery algorithm, integers are used for fair schedulers of concurrent processes. In this paper, we present the extension of a fair scheduler from `static control' (the number of processes is fixed) to `dynamic control' (the number of processes changes during execution). We believe that our results shed new light on the concept of fairness in the setting of dynamic control.
[HHP10]: M. Heizmann, J. Hoenicke, and A. Podelski. Nested interpolants. In POPL 10, pages 471-482. ACM, 2010. [ bib | DOI | .pdf ]
In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare proofs and predicate abstraction in the context of recursive programs. Our technical contribution is an interpolant-based software model checking method for recursive programs. The method avoids the costly construction of the abstract transformer by constructing a nested word automaton from an inductive sequence of `nested interpolants' (i.e., interpolants for a nested word which represents an infeasible error trace).
[HLP⁺09]: J. Hoenicke, K.R.M. Leino, A. Podelski, M. Schäf, and T. Wies. It's doomed; we can prove it. In FM 2009, number 5850 in LNCS, pages 338-353. Springer, 2009. [ bib | DOI | .pdf ]
Programming errors found early are the cheapest. Tools applying to the early stage of code development exist but either they suffer from false positives (“noise”) or they require strong user interaction. We propose to avoid this deficiency by defining a new class of errors. A program fragment is doomed if an execution that reaches it, in whatever state, will inevitably fail. We use a formal verification method to identify such errors fully automatically and, most significantly, without producing noise. We report on preliminary experiments with a prototypical tool.
[HHP09]: M. Heizmann, J. Hoenicke, and A. Podelski. Refinement of trace abstraction. In Static Analysis Symposium (SAS 2009), number 5673 in LNCS, pages 69-85. Springer, 2009. [ bib | DOI | .pdf ]
Automatic refinement of abstraction is an active research theme in static analysis. In existing approaches, calls to theorem provers (for the construction of a sequence of increasingly precise state abstractions) represent an obstacle to scalability. We present an approach that aims at the reuse of theorem prover calls. The abstraction is based not on states but on traces. Each refinement extends a tuple of automata with another automaton; this automaton is derived from the interpolant-based analysis of a spurious counterexample.
[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. [ bib | DOI ]
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).
[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 | DOI | .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.
[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, May 2002. [ bib | DOI | .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 | .pdf ]
We use a combination of three techniques for the specification of processes, data and time: CSP, Object-Z and Duration Calculus. Whereas the combination of CSP and Object-Z is well established by the work of C. Fischer, the integration with Duration Calculus is new. The combination is used to specify parts of a novel case study on radio controlled railway crossings.

Theses

[Hoe06]: Jochen Hoenicke. Combination of Processes, Data, and Time. PhD thesis, University of Oldenburg, July 2006. [ bib | .pdf ]
[Hoe99]: Jochen Hoenicke. Graphische Spezifikationsspachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams. Master's thesis, 1999. [ bib | .pdf ]