Model-Checking of Specifications Integrating Processes, Data and Time

Jochen Hoenicke, Patrick Maier

Research output: Chapter in Book/Report/Conference proceedingConference contribution

17 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationFM 2005: Formal Methods
Subtitle of host publicationInternational Symposium of Formal Methods Europe; Newcastle, UK, July 18-22, 2005; Proceedings
EditorsJohn Fitzgerald, Ian J Hayes, Andrzej Tarlecki
Number of pages16
ISBN (Electronic)978-3-540-31714-2
ISBN (Print)978-3-540-27882-5
Publication statusPublished - Jul 2005
EventFormal Methods 2005, FM 2005 - Newcastle upon Tyne, United Kingdom
Duration: 18 Jul 200522 Jul 2005

Publication series

NameLecture Notes in Computer Science


ConferenceFormal Methods 2005, FM 2005
Country/TerritoryUnited Kingdom
CityNewcastle upon Tyne


  • combination of specification languages
  • CSP
  • Object-Z
  • Duration Calculus
  • model checking


Dive into the research topics of 'Model-Checking of Specifications Integrating Processes, Data and Time'. Together they form a unique fingerprint.

Cite this