Publications
Publications
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: bib2bib -ob publications.bib -c author:"Hoenicke" all.bib names-long.bib}}
@inproceedings{PH12,
author = {Amalinda Post and Jochen Hoenicke},
title = {Formalization and Analysis of Real-Time Requirements: a Feasibility Study at {BOSCH}},
booktitle = {VSTTE 12},
publisher = {Springer},
series = {LNCS},
year = {2012},
optpages = {?},
abstract = {
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 \textsc{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.
},
note = {To appear},
optdoi = {}
}
@inproceedings{EHP12,
author = {Evren Ermis and Jochen Hoenicke and Andreas Podelski},
title = {Splitting via Interpolants},
booktitle = {VMCAI 12},
publisher = {Springer},
series = {LNCS},
year = {2012},
optpages = {?},
abstract = {
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 \emph{path insensitive} interpolation to compute loop invariants.
In contrast to current approaches, path insensitive interpolation summarizes
\emph{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.
},
note = {To appear},
optdoi = {}
}
@inproceedings{PHP11b,
author = {Amalinda Post and Jochen Hoenicke and Andreas Podelski},
title = {Vacuous real-time requirements},
booktitle = {RE 11},
publisher = {IEEE},
year = {2011},
pages = {153--162},
abstract = {
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.
},
doi = {10.1109/RE.2011.6051657}
}
@inproceedings{PHP11,
author = {Amalinda Post and Jochen Hoenicke and Andreas Podelski},
title = {{rt}-inconsistency: a new property for real-time requirements},
booktitle = {FASE 2011},
year = {2011},
publisher = {Springer},
series = {LNCS},
number = {6603},
pages = {34--49},
abstract = {
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
\textsc{Bosch}. The case study demonstrates the relevance of rt-inconsistency
for detecting errors in industrial real-time requirements specifications.
},
doi = {10.1007/978-3-642-19811-3_4}
}
@article{HLPSW10,
author = {J. Hoenicke and K.R.M. Leino and A. Podelski and M. Sch\"af and T. Wies},
title = {Doomed Program Points},
journal = {Formal Methods in System Design},
volume = 37,
number = {2--3},
month = {December},
pages = {171--199},
year = {2010},
publisher = {Springer},
abstract = {
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.
},
doi = {10.1007/s10703-010-0102-0}
}
@inproceedings{HMO10,
author = {J. Hoenicke and R. Meyer and E.-R. Olderog},
title = {{K}leene, {R}abin, and {S}cott are available},
booktitle = {CONCUR 2010},
opteditor = {Paul Gastin and Fran\c{c}ois Laroussinie},
year = {2010},
publisher = {Springer},
series = {LNCS},
number = {6269},
pages = {462--477},
abstract = {
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.
},
doi = {10.1007/978-3-642-15375-4_32}
}
@inproceedings{HOP10,
author = {J. Hoenicke and E.-R. Olderog and A. Podelski},
title = {Fairness for Dynamic Control},
booktitle = {TACAS 2010},
year = {2010},
publisher = {Springer},
series = {LNCS},
number = {6015},
pages = {251--265},
abstract = {
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.
},
doi = {10.1007/978-3-642-12002-2_20}
}
@inproceedings{HHP10,
author = {M. Heizmann and J. Hoenicke and A. Podelski},
title = {Nested Interpolants},
booktitle = {POPL 10},
pages = {471--482},
year = {2010},
publisher = {ACM},
abstract = {
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).
},
doi = {10.1145/1706299.1706353},
url = {docs/hhp10-popl.pdf}
}
@inproceedings{HLPSW09,
author = {J. Hoenicke and K.R.M. Leino and A. Podelski and M. Sch\"af and T. Wies},
title = {It's Doomed; we can Prove it},
booktitle = {FM 2009},
number = {5850},
pages = {338--353},
year = {2009},
publisher = {Springer},
series = {LNCS},
abstract = {
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.
},
doi = {10.1007/978-3-642-05089-3_22},
url = {docs/hlpsw09-fm.pdf}
}
@inproceedings{HHP09,
author = {M. Heizmann and J. Hoenicke and A. Podelski},
title = {Refinement of Trace Abstraction},
booktitle = {Static Analysis Symposium (SAS 2009)},
number = {5673},
pages = {69--85},
year = {2009},
publisher = {Springer},
series = {LNCS},
abstract = {
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.
},
doi = {10.1007/978-3-642-03237-0_7},
url = {docs/hhp09-sas.pdf}
}
@article{MFHR08,
author = {R. Meyer and J. Faber and J. Hoenicke and A. Rybalchenko},
title = {Model Checking {D}uration {C}alculus: a practical approach},
journal = {Formal Aspects of Computing},
year = {2008},
volume = {20},
number = {4--5},
month = {July},
pages = {481--505},
publists = {meyer,faber,hoenicke},
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}
}
@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 = {docs/hm05-fm.pdf},
doi = {10.1007/11526841_31},
publists = {pea},
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.
}
}
@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,
doi = {10.1007/3-540-47884-1_14},
url = {docs/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 = {docs/fbt01.pdf},
abstract = {
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
@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: bib2bib -ob publications.bib -c author:"Hoenicke" theses.bib names-long.bib}}
@phdthesis{jh2006,
author = {Jochen Hoenicke},
title = {{Combination of Processes, Data, and Time}},
school = {University of Oldenburg},
url = {docs/csp-oz-dc.pdf},
month = {July},
year = {2006}
}
@mastersthesis{jh99-mt,
author = {Jochen Hoenicke},
title = {{Graphische Spezifikationsspachen: Der Zusammenhang zwischen Constraint Diagrams und Real-Time Symbolic Timing Diagrams}},
url = {docs/diplom.pdf},
school = uniol-fb10,
year = 1999
}
