M. Oliver Möller
Model-based development is hindered mainly by the lack of adequate modeling languages and the high computational cost of the analysis. In this thesis we improve the situation along both axes.
First, we bring the mathematical model closer to the human designer. This we achieve by casting hierarchical structures--as known from statechart-like formalisms--into a formal timed model. This shapes a high-level language, which allows for fully automated verification.
Second, we use sound approximations to achieve more efficient automation in the verification of timed properties. We present two novel state-based techniques that have the potential to reduce time and memory consumption drastically.
The first technique makes use of structural information, in particular loops, to exploit regularities in the reachable state space. Via shortcut-like additions to the model we avoid repetition of similar states during an exhaustive state space exploration.
The second technique applies the abstract interpretation framework to a real-time setting. We preserve the control structure and approximate only the more expensive time component of a state. The verification of infinite behavior, also known as liveness properties, requires an assumption on the progress of time. We incorporate this assumption by means of limiting the behavior of the model with respect to delay steps. For a next-free temporal logic, this modification does not change the set of valid properties.
We supplement our research with experimental run-time data. This data is gathered via prototype implementations on top of the model checking tools UPPAAL and MOCHA
Available as PDF.