Model-Checking of Specifications Integrating Processes, Data and Time

Jochen Hoenicke, Patrick Maier

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

14 Citations (Scopus)

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.
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
PublisherSpringer
Pages465-480
Number of pages16
Volume3582
ISBN (Electronic)978-3-540-31714-2
ISBN (Print)978-3-540-27882-5
DOIs
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
PublisherSpringer

Conference

ConferenceFormal Methods 2005, FM 2005
CountryUnited Kingdom
CityNewcastle upon Tyne
Period18/07/0522/07/05

Keywords

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

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

  • Cite this

    Hoenicke, J., & Maier, P. (2005). Model-Checking of Specifications Integrating Processes, Data and Time. In J. Fitzgerald, I. J. Hayes, & A. Tarlecki (Eds.), FM 2005: Formal Methods: International Symposium of Formal Methods Europe; Newcastle, UK, July 18-22, 2005; Proceedings (Vol. 3582, pp. 465-480). (Lecture Notes in Computer Science). Springer. https://doi.org/10.1007/11526841_31