Model checking the FlexRay startup phase

S. Cranen

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

8 Citations (Scopus)
7 Downloads (Pure)

Abstract

The FlexRay protocol is an upcoming standard in automotive industry. Its specification is finalised and maintained by ISO. It is a time-triggered protocol that uses a fault-tolerant clock synchronisation mechanism. During a startup phase that should be resilient to certain faults, the clocks in the network are synchronised and the protocol is initialised. This paper presents a model of the startup phase of the protocol in the mCRL2 modelling language, and shows how model checking techniques can be used to check that the startup protocol fulfills the requirements. A previously unknown scenario is uncovered in which a single failing node can cause another node, or even the entire network, not to start up.
Original languageEnglish
Title of host publicationFormal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings)
EditorsM. Stoelinga, R. Pinger
Place of PublicationBerlin
PublisherSpringer
Pages131-145
ISBN (Print)978-3-642-32468-0
DOIs
Publication statusPublished - 2012
Event17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012) - Paris, France
Duration: 27 Aug 201228 Aug 2012
Conference number: 17

Publication series

NameLecture Notes in Computer Science
Volume7437
ISSN (Print)0302-9743

Conference

Conference17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012)
Abbreviated titleFMCIS 2012
CountryFrance
CityParis
Period27/08/1228/08/12

Fingerprint Dive into the research topics of 'Model checking the FlexRay startup phase'. Together they form a unique fingerprint.

  • Cite this

    Cranen, S. (2012). Model checking the FlexRay startup phase. In M. Stoelinga, & R. Pinger (Eds.), Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings) (pp. 131-145). (Lecture Notes in Computer Science; Vol. 7437). Springer. https://doi.org/10.1007/978-3-642-32469-7_9