Structure and Hierarchy in Real-Time Systems


written by M. Oliver M"oller 
	in Partial Fulfilment of the Requirements for the PhD Degree
Aarhus, 20 Februar 2002.


Abstract.

The development of digital systems is particularly challenging, if their
correctness depends on the right timing of operations. One approach to
enhance the reliability of such systems is model-based development. This
allows for a formal analysis throughout all stages of design.


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