Model-Checking of Specifications Integrating Processes, Data and Time

Hoenicke, Jochen; Maier, Patrick; Fitzgerald, John; Hayes, Ian J.; Tarlecki, Andrzej

Item

ITEM ACTIONSEXPORT

Add to Basket

Local TagsRelease HistoryDetailsSummary

Released

Conference Paper

Model-Checking of Specifications Integrating Processes, Data and Time

MPS-Authors

/persons/resource/persons44629

Hoenicke, Jochen
Programming Logics, MPI for Informatics, Max Planck Society;

/persons/resource/persons44970

Maier, Patrick
Programming Logics, MPI for Informatics, Max Planck Society;

External Resource

No external resources are shared

Fulltext (restricted access)

There are currently no full texts shared for your IP range.

Fulltext (public)

There are no public fulltexts stored in PuRe

Supplementary Material (public)

There is no public supplementary material available

Citation

Hoenicke, J., & Maier, P. (2005). Model-Checking of Specifications Integrating Processes, Data and Time. In FM 2005: Formal Methods; International Symposium of Formal Methods Europe (pp. 465-480). Berlin, Germany: Springer.

Cite as: https://hdl.handle.net/11858/00-001M-0000-000F-2715-6

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.