Verification of FlexRay start-up mechanism by timed automata

• Autorzy: Malinský J. , Novák J.
• Języki publikacji: EN

Abstrakty

EN

This contribution deals with the modelling of a selected part of a new automotive communication standard called FlexRay. In particular, it focuses on the mechanism ensuring the start-up of a FlexRay network. The model has been created with the use of timed automata and verified. For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of suitable queries compiled in the so called computation tree logic. This model can be used to look for incorrect settings of time parameters of communication nodes in the network that prevent network start-up and subsequently the start of the car. The existence of this model also opens the way for finding possible errors in the standard. On the basis of the model, the work gives a case study of the start-up mechanism behaviour verification in a FlexRay network consisting of three communication nodes.

Słowa kluczowe

EN

FlexRay; Timed Automata; modelling

• Wydawca: Komitet Metrologii i Aparatury Naukowej PAN
• Czasopismo: Metrology and Measurement Systems
• Rocznik: 2010
• Tom: Vol. 17, nr 3
• Strony: 461--480
• Opis fizyczny: Bibliogr. 13 poz., rys., tab.

Twórcy

autor

Malinský J.

autor

Novák J.

• Czech Technical University, Faculty of Electrical Engineering, Technická 2, 166 27 Prague 6, Czech Republic,

Bibliografia

• [1] T. Hiaroka, S. Eto, O. Nishihara, H.Kumamoto: “Fault Tolerant Design for X-by-wire Vehicle”. SICE 2004 Annual Conference, Hokkaido Institute of Technology, Sapporo, Japan, vol. 3, Aug. 2004, pp. 1940-1945.
• [2] H. Kopetz: A Comparison of TTP/C and FlexRay. Technical report 10/2001 Vienna University of Technology, Real-Time System Group.
• [3] FlexRay Consortium, “FlexRay Protocol Specification v.2.1 Rev. A”, FlexRay Consortium, 2005.
• [4] FlexRay Consortium, “FlexRay Electrical Physical Layer Specification v.2.1 Rev. A”, Flex Ray Consortium, 2005.
• [5] UPPSALA University, AALBORG University: UPPAAL - integrated tool environment for modelling, validation and verification of real-time systems modelled as networks of timed automata. Available at: www.uppaal.com.
• [6] G. Behrmann, A. David, K.G. Larsen: A tutorial on Uppaal. Department of Computer Science. Aalborg University, Denmark.
• [7] R. Alur, D.L. Dill: “A theory of timed automata”. Theoretical Computer Science, vol. 126, no. 2, Apr. 1994, pp. 183-235.
• [8] R. Alur, C. Courcoubetis, D.L. Dill: “Model-checking for realtime systems”. 5th Symposium on Logic in Computer Science, 1990, pp. 414-425.
• [9] J. Krakora, L. Waszniowski, Z. Hanzalek: “Timed Automata Approach to Distributed and Fault Tolerant System Verification”. 1st NeCTS Workshop, Networked Control Systems & Fault Tolerant Control, 2005, pp. 45-50.
• [10] J. Krakora, Z. Hanzalek: “Checking Real-Time Properties of CAN Bus by Timed automata”. Advanced Control Theory and Applications, 2003, pp. 130-134.
• [11] J. Krakora, Z. Hanzalek: “Testing of Hybrid Real - time System Using FPGA Platform”. IEEE Symposium on Industrial Embedded Systems - IES 2006, Lyon, CNRS-ENS, 2006. CD-ROM
• [12]K. Godary, P. Parrend, I. Augé-Blum: “Comparison and Temporal Validation of Automotive Real-Time Architectures”. International Conference on Industrial Technology, Hammamet, Tunisia, Dec. 2004.
• [13] J. Malinský: “The application of the timed automata for FlexRay start-up testing”. 16th IMEKO TC4 Symposium, Florence, pp. 425-430. CD-ROM