Model checking the FlexRay startup phase

S. Cranen

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

    10 Citations (Scopus)
    7 Downloads (Pure)


    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
    ISBN (Print)978-3-642-32468-0
    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
    ISSN (Print)0302-9743


    Conference17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012)
    Abbreviated titleFMCIS 2012


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

    Cite this