Model checking the FlexRay startup phase

S. Cranen

doi:10.1007/978-3-642-32469-7_9

Model checking the FlexRay startup phase

S. Cranen

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

9 Citaten (Scopus)

7 Downloads (Pure)

Samenvatting

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.

Originele taal-2	Engels
Titel	Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings)
Redacteuren	M. Stoelinga, R. Pinger
Plaats van productie	Berlin
Uitgeverij	Springer
Pagina's	131-145
ISBN van geprinte versie	978-3-642-32468-0
DOI's	https://doi.org/10.1007/978-3-642-32469-7_9
Status	Gepubliceerd - 2012
Evenement	17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012) - Paris, Frankrijk Duur: 27 aug. 2012 → 28 aug. 2012 Congresnummer: 17

Publicatie series

Naam	Lecture Notes in Computer Science
Volume	7437
ISSN van geprinte versie	0302-9743

Congres

Congres	17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012)
Verkorte titel	FMCIS 2012
Land/Regio	Frankrijk
Stad	Paris
Periode	27/08/12 → 28/08/12
Ander	17th International Workshop on Formal Methods for Industrial Critical Systems

Toegang tot document

10.1007/978-3-642-32469-7_9

Citeer dit

@inproceedings{6ab41607cc5f4c41bae291037de68b1e,

title = "Model checking the FlexRay startup phase",

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

author = "S. Cranen",

year = "2012",

doi = "10.1007/978-3-642-32469-7_9",

language = "English",

isbn = "978-3-642-32468-0",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "131--145",

editor = "M. Stoelinga and R. Pinger",

booktitle = "Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings)",

address = "Germany",

note = "17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012), FMCIS 2012 ; Conference date: 27-08-2012 Through 28-08-2012",

}

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

Model checking the FlexRay startup phase. / Cranen, S.

Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings). redactie / M. Stoelinga; R. Pinger. Berlin : Springer, 2012. blz. 131-145 (Lecture Notes in Computer Science; Vol. 7437).

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/Congresprocedure › Conferentiebijdrage › Academic › peer review

TY - GEN

T1 - Model checking the FlexRay startup phase

AU - Cranen, S.

N1 - Conference code: 17

PY - 2012

Y1 - 2012

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

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

U2 - 10.1007/978-3-642-32469-7_9

DO - 10.1007/978-3-642-32469-7_9

M3 - Conference contribution

SN - 978-3-642-32468-0

T3 - Lecture Notes in Computer Science

SP - 131

EP - 145

BT - Formal Methods for Industrial Critical Systems (17th International Workshop, FMICS 2012, Paris, France, August 27-28, 2012. Proceedings)

A2 - Stoelinga, M.

A2 - Pinger, R.

PB - Springer

CY - Berlin

T2 - 17th International Workshop on Formal Methods for Industrial Critical Systems (FMCIS 2012)

Y2 - 27 August 2012 through 28 August 2012

ER -

Model checking the FlexRay startup phase

Samenvatting

Publicatie series

Congres

Toegang tot document

Vingerafdruk

Citeer dit