Model Checking the FlexRay Physical Layer Protocol
Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter
The FlexRay standard, developed by a cooperation of leading companies in the automotive industry, is a robust communication protocol for distributed components in modern vehicles. In this paper, we present the first timed automata model of its physical layer protocol, and we use automatic verification to prove fault tolerance under several error models and hardware assumptions. The key challenge in the analysis is that the correctness of the protocol relies on the interplay of the bit-clock alignment mechanism with the precise timing behavior of the underlying asynchronous hardware. We give a general hardware model that is parameterized in low-level timing details such as hold times and propagation delays. Instantiating this model for a realistic design from the Nangate Open Cell Library, and verifying the resulting model using the real-time model checker Uppaal, we show that the communication system meets, and in fact exceeds, the fault-tolerance guarantees claimed in the FlexRay specification.
15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010).
Copyright by Springer Verlag. The original publication is available at www.springerlink.com.