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.
The work in this paper is supported by the Dutch HTAS-VERIFIED project, see http://www.htas.nl/index.php?pid=154.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Barsotti, D., Nieto, L., Tiu, A.: Verification of Clock Synchronization Algorithms: Experiments on a combination of deductive tools. Formal Aspects of Computing 19(3), 321–341 (2007)
Botaschanjan, J., Broy, M., Gruler, A., Harhurin, A., Knapp, S., Kof, L., Paul, W., Spichkova, M.: On the correctness of upper layers of automotive systems. Formal Aspects of Computing 20(6), 637–662 (2008)
Botaschanjan, J., Gruler, A., Harhurin, A., Kof, L., Spichkova, M., Trachtenherz, D.: Towards Modularized Verification of Distributed Time-Triggered Systems. In: Misra, J., Nipkow, T., Karakostas, G. (eds.) FM 2006. LNCS, vol. 4085, pp. 163–178. Springer, Heidelberg (2006)
Broy, M., Stølen, K.: Specification and development of interactive systems: focus on streams, interfaces, and refinement. Springer (2001)
Cranen, S.: Model checking the flexray startup phase. Technical Report 12-01, Eindhoven University of Technology (2012)
Cranen, S., Keiren, J.J.A., Willemse, T.A.C.: Stuttering Mostly Speeds Up Solving Parity Games. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 207–221. Springer, Heidelberg (2011)
Flexray consortium: FlexRay Preliminary Node Local Bus Guardian Specification v2.0.9 (2005)
Flexray consortium: FlexRay Requirements Specification v2.1 (2005)
Flexray consortium: FlexRay Protocol Specification v3.0.1 (2010)
Fontaine, P., Gupta, K., Marion, J., Merz, S., Nieto, L., Tiu, A.: Towards a combination of heterogeneous deductive tools for system verification: A case study on clock synchronization. In: APPSEM Workshop, Citeseer (2005)
Groote, J., Mateescu, R.: Verification of temporal properties of processes in a setting with data. In: AMAST, pp. 74–90 (1998)
ITU-T: Recommendation Z.100: Specification and Description Language (SDL) (1999)
Kühnel, C., Spichkova, M.: FlexRay und FTCom: Formale Spezifikation in FOCUS. Technical report, Technische Universität München (2006)
Kühnel, C., Spichkova, M.: Upcoming Automotive Standards for Fault-Tolerant Communication: FlexRay and OSEKTime FTCom. In: EFTS 2006 International Workshop on Engineering of Fault Tolerant Systems. Universite du Luxembourg, CSC: Computer Science and Communication (2006)
Lundelius, J., Lynch, N.: A new fault-tolerant algorithm for clock synchronization. In: Proc. 3rd ACM Symposium on Principles of Distributed Computing, p. 88. ACM (1984)
Malinský, J., Novák, J.: Verification of flexray start-up mechanism by timed automata. Metrology and Measurement Systems XVII(3), 461–480 (2010)
Spichkova, M.: FlexRay: Verification of the FOCUS Specification in Isabelle/HOL. A Case Study. Technical report, Technische Universität München (2006)
Steiner, W.: An assessment of FlexRay 2.0 (safety aspects). Technical Report 45/2005, Technische Universität Wien (2005)
Steiner, W.: Model-checking studies of the FlexRay startup algorithm. Technical Report 57/200, Technische Universität Wien (2005)
Zhang, B.: On the Formal Verification of the FlexRay Communication Protocol. In: Automatic Verification of Critical Systems (AVoCS), pp. 184–189 (2006)
Zhang, B.: Specifying and Verifying Timing Properties of a Time-triggered Protocol for In-vehicle Communication. In: Proceedings of the 2008 Ninth ACIS International Conference on Software Engineering, Artificial Intelligence, Networking, and Parallel/Distributed Computing, pp. 467–472. IEEE Computer Society (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cranen, S. (2012). Model Checking the FlexRay Startup Phase. In: Stoelinga, M., Pinger, R. (eds) Formal Methods for Industrial Critical Systems. FMICS 2012. Lecture Notes in Computer Science, vol 7437. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32469-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-32469-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32468-0
Online ISBN: 978-3-642-32469-7
eBook Packages: Computer ScienceComputer Science (R0)