Automatic Protocol Verification with Parametric Physical Layers
Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter
The FlexRay standard describes a robust communication protocol for distributed components. Originally developed for the automotive industry, FlexRay recently attracted a lot of attention in the aeronautics industry. In this much more sensitive domain, however, some standard assumptions (concerning, e.g., the maximal harness length) easily exceed the limits specified in the original standard.
In this paper, we advocate to use model checking as the key technique to automatically establish the correctness of an asynchronous communication protocol that is parametric in its environment assumptions. For this purpose, we present a general methodology for an efficient modeling of communication protocols with parametric physical layers. As a case study, we apply these guidelines to obtain a model of FlexRay’s physical layer protocol based on timed automata. Using the model checker Uppaal, we are able to establish new results that significantly extend the rather conservative assumptions in the standard.