Embedded software analysis with MOTOR

Joost-Pieter Katoen; Henrik Bohnenkamp; Ric Klaren; Holger Hermanns

doi:10.1007/b110123

Embedded software analysis with MOTOR

Joost-Pieter Katoen, Henrik Bohnenkamp, Ric Klaren, Holger Hermanns

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

2 Citations (Scopus)

170 Downloads (Pure)

Abstract

This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

Original language	English
Title of host publication	Formal Methods for the Design of Real-Time Systems
Subtitle of host publication	International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures
Editors	Marco Bernardo, Flavio Corradini
Publisher	Springer
Pages	268-293
Number of pages	26
ISBN (Electronic)	978-3-540-30080-9
ISBN (Print)	978-3-540-23068-8-7
DOIs	https://doi.org/10.1007/b110123
Publication status	Published - 2004
Event	International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004 - Bertinoro, Italy Duration: 13 Sept 2004 → 18 Sept 2004

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	3185
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004
Abbreviated title	SFM-RT
Country/Territory	Italy
City	Bertinoro
Period	13/09/04 → 18/09/04

Keywords

FMT-PM: PROBABILISTIC METHODS
FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS
FMT-TOOLS
Model checker
Operational semantics
Overlay networks
Critical section
Mutual exclusion

Access to Document

10.1007/b110123

Katoen2004embeddedAccepted author version, 433 KB

Cite this

Katoen, J-P., Bohnenkamp, H., Klaren, R., & Hermanns, H. (2004). Embedded software analysis with MOTOR. In M. Bernardo, & F. Corradini (Eds.), Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures (pp. 268-293). (Lecture Notes in Computer Science; Vol. 3185). Springer. https://doi.org/10.1007/b110123

Katoen, Joost-Pieter ; Bohnenkamp, Henrik ; Klaren, Ric et al. / Embedded software analysis with MOTOR. Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures. editor / Marco Bernardo ; Flavio Corradini. Springer, 2004. pp. 268-293 (Lecture Notes in Computer Science).

@inbook{58ddf7ae32b24f2181b2207682aaef21,

title = "Embedded software analysis with MOTOR",

abstract = "This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.",

keywords = "FMT-PM: PROBABILISTIC METHODS, FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS, FMT-TOOLS, Model checker, Operational semantics, Overlay networks, Critical section, Mutual exclusion",

author = "Joost-Pieter Katoen and Henrik Bohnenkamp and Ric Klaren and Holger Hermanns",

year = "2004",

doi = "10.1007/b110123",

language = "English",

isbn = "978-3-540-23068-8-7",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "268--293",

editor = "Marco Bernardo and Flavio Corradini",

booktitle = "Formal Methods for the Design of Real-Time Systems",

note = "International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, SFM-RT ; Conference date: 13-09-2004 Through 18-09-2004",

}

Katoen, J-P, Bohnenkamp, H, Klaren, R & Hermanns, H 2004, Embedded software analysis with MOTOR. in M Bernardo & F Corradini (eds), Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures. Lecture Notes in Computer Science, vol. 3185, Springer, pp. 268-293, International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, 13/09/04. https://doi.org/10.1007/b110123

Embedded software analysis with MOTOR. / Katoen, Joost-Pieter; Bohnenkamp, Henrik; Klaren, Ric et al.
Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures. ed. / Marco Bernardo; Flavio Corradini. Springer, 2004. p. 268-293 (Lecture Notes in Computer Science; Vol. 3185).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-review

TY - CHAP

T1 - Embedded software analysis with MOTOR

AU - Katoen, Joost-Pieter

AU - Bohnenkamp, Henrik

AU - Klaren, Ric

AU - Hermanns, Holger

PY - 2004

Y1 - 2004

N2 - This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

AB - This paper surveys the language Modest, a Modelling and Description language for Stochastic and Timed systems, and its accompanying tool-environment MOTOR. The language and tool are aimed to support the modular description and analysis of reactive systems while covering both functional and non-functional system aspects such as hard and soft real-time, and quality-of-service aspects. As an illustrative example, the modeling and analysis of a device-absence detecting protocol in plug-and-play networks is described and is shown to exhibit some undesired behaviour.

KW - FMT-PM: PROBABILISTIC METHODS

KW - FMT-FMPA: FORMAL METHODS FOR PERFORMANCE ANALYSIS

KW - FMT-TOOLS

KW - Model checker

KW - Operational semantics

KW - Overlay networks

KW - Critical section

KW - Mutual exclusion

U2 - 10.1007/b110123

DO - 10.1007/b110123

M3 - Chapter

SN - 978-3-540-23068-8-7

T3 - Lecture Notes in Computer Science

SP - 268

EP - 293

BT - Formal Methods for the Design of Real-Time Systems

A2 - Bernardo, Marco

A2 - Corradini, Flavio

PB - Springer

T2 - International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004

Y2 - 13 September 2004 through 18 September 2004

ER -

Katoen J-P, Bohnenkamp H, Klaren R, Hermanns H. Embedded software analysis with MOTOR. In Bernardo M, Corradini F, editors, Formal Methods for the Design of Real-Time Systems: International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT 2004, Bertinoro, Italy, September 13-18, 2004. Revised Lectures. Springer. 2004. p. 268-293. (Lecture Notes in Computer Science). doi: 10.1007/b110123

Embedded software analysis with MOTOR

Abstract

Publication series

Conference

Keywords

Access to Document

Fingerprint

Cite this