FlexRay for Avionics: Automatic Verification with Parametric Physical Layers
Michael Gerke, Rüdiger Ehlers, Bernd Finkbeiner, and Hans-Jörg Peter
The automotive FlexRay standard is increasingly attracting attention in the aeronautics industry. Upgrading existing physical layers, such as CAN-based systems, with FlexRay is attractive, especially given that inexpensive FlexRay hardware is available on the market. However, such a change of the application context requires a careful examination of the assumptions the protocol is based on. For example, the FlexRay standard assumes that the harness length is at most 24 meters, a requirement that is typically met by ground vehicles but not by planes. In this paper, we present a methodology for the formal analysis of the impact of changes to the physical setting on the fault tolerance of the protocol. We use the real-time model checker Uppaal to automatically verify the behavior of the FlexRay physical layer protocol when executed on a range of hardware configurations. We report on design considerations and lessons learned in building a model that is sufficiently small to allow for automatic verification and, at the same time, sufficiently precise to describe the intricate real-time interplay of protocol and hardware.
American Institute of Aeronautics and Astronautics: Infotech@Aerospace 2012 (I@A 2012).