Specifying and Verifying Timing Properties of a Time-triggered Protocol for In-vehicle Communication

In order to achieve predictability, time-triggered communication systems have been proposed for use in in-vehicle applications, in particular for safety-critical applications. Timing properties play a crucial role in a time-triggered system as activities in such a system are all triggered by the passage of time. In this paper, we propose techniques for specifying and verifying the timing properties of the FlexRay protocol, an emerging time-triggered communication protocol for automotive systems. Essential timing properties of the protocol are defined and proved. Mechanical support with the theorem prover Isabelle/HOL is also considered.