Model-Checking of Specifications Integrating Processes, Data and Time

Jochen Hoenicke; Patrick Maier

doi:10.1007/11526841_31

Model-Checking of Specifications Integrating Processes, Data and Time

Jochen Hoenicke, Patrick Maier

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

17 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 language	English
Title of host publication	FM 2005: Formal Methods
Subtitle of host publication	International Symposium of Formal Methods Europe; Newcastle, UK, July 18-22, 2005; Proceedings
Editors	John Fitzgerald, Ian J Hayes, Andrzej Tarlecki
Publisher	Springer
Pages	465-480
Number of pages	16
Volume	3582
ISBN (Electronic)	978-3-540-31714-2
ISBN (Print)	978-3-540-27882-5
DOIs	https://doi.org/10.1007/11526841_31
Publication status	Published - Jul 2005
Event	Formal Methods 2005, FM 2005 - Newcastle upon Tyne, United Kingdom Duration: 18 Jul 2005 → 22 Jul 2005

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer

Conference

Conference	Formal Methods 2005, FM 2005
Country/Territory	United Kingdom
City	Newcastle upon Tyne
Period	18/07/05 → 22/07/05

Keywords

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

Access to Document

10.1007/11526841_31

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

@inproceedings{2efcb94872e64ef48ededd2396d85e35,

title = "Model-Checking of Specifications Integrating Processes, Data and Time",

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.",

keywords = "combination of specification languages, CSP, Object-Z, Duration Calculus, model checking",

author = "Jochen Hoenicke and Patrick Maier",

year = "2005",

month = jul,

doi = "10.1007/11526841_31",

language = "English",

isbn = "978-3-540-27882-5",

volume = "3582",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "465--480",

editor = "Fitzgerald, {John } and Hayes, {Ian J} and Tarlecki, {Andrzej }",

booktitle = "FM 2005: Formal Methods",

note = "Formal Methods 2005, FM 2005 ; Conference date: 18-07-2005 Through 22-07-2005",

}

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

Model-Checking of Specifications Integrating Processes, Data and Time. / Hoenicke, Jochen; Maier, Patrick.
FM 2005: Formal Methods: International Symposium of Formal Methods Europe; Newcastle, UK, July 18-22, 2005; Proceedings. ed. / John Fitzgerald; Ian J Hayes; Andrzej Tarlecki. Vol. 3582 Springer, 2005. p. 465-480 (Lecture Notes in Computer Science).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - Model-Checking of Specifications Integrating Processes, Data and Time

AU - Hoenicke, Jochen

AU - Maier, Patrick

PY - 2005/7

Y1 - 2005/7

N2 - 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.

AB - 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.

KW - combination of specification languages

KW - CSP

KW - Object-Z

KW - Duration Calculus

KW - model checking

U2 - 10.1007/11526841_31

DO - 10.1007/11526841_31

M3 - Conference contribution

SN - 978-3-540-27882-5

VL - 3582

T3 - Lecture Notes in Computer Science

SP - 465

EP - 480

BT - FM 2005: Formal Methods

A2 - Fitzgerald, John

A2 - Hayes, Ian J

A2 - Tarlecki, Andrzej

PB - Springer

T2 - Formal Methods 2005, FM 2005

Y2 - 18 July 2005 through 22 July 2005

ER -

Model-Checking of Specifications Integrating Processes, Data and Time

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this