ausblenden:
Schlagwörter:
-
Zusammenfassung:
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.
