Model-checking of specifications integrating processes, data and time. (English) Zbl 1120.68417

Fitzgerald, John (ed.) et al., FM 2005: Formal methods. International symposium of formal methods Europe, Newcastle, UK, July 18–22, 2005. Proceedings. Berlin: Springer (ISBN 3-540-27882-6/pbk). Lecture Notes in Computer Science 3582, 465-480 (2005).
Summary: 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.
For the entire collection see [Zbl 1078.68005].


68Q60 Specification and verification (program logics, model checking, etc.)


Moby/DC; Kronos; SLAM
Full Text: DOI