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 language | English |
|---|---|
| Title of host publication | Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings) |
| Editors | M. Stoelinga, R. Pinger |
| Place of Publication | Berlin |
| Publisher | Springer |
| Pages | 131-145 |
| ISBN (Print) | 978-3-642-32468-0 |
| DOIs | |
| Publication status | Published - 2012 |
| Event | 17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012) - Paris, France Duration: 27 Aug 2012 → 28 Aug 2012 Conference number: 17 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Volume | 7437 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012) |
|---|---|
| Abbreviated title | FMCIS 2012 |
| Country/Territory | France |
| City | Paris |
| Period | 27/08/12 → 28/08/12 |