Modeling and verification of a time-triggered networking protocol

Analysis estimates that more than 80% of all current innovations within vehicles are based on distributed electronic systems. Critical to the functionality and application domain of such systems is the underlying communication network. Current advances in control networking technology indicate that time-triggered architectures offer improvements in deterministic behaviour, which are particularly appropriate for safety-critical and real-time applications. Here we present novel work on the formal specification and formal verification of a time-triggered protocol: ISO 11898-4 - Time Triggered communication on the Controller Area Network (TTCAN)®. This work has been carried out using the UPPAAL model checker based tool set which is capable of verifying safety properties as formalised by simple reachability properties. These verifiable properties are a subset of those possible in a full realisation of Timed Computation Tree Logic (TCTL). Three TTCAN network automata and a medium automaton were designed. Nine properties including deadlock were examined. The results provide a high degree of confidence in the correctness of the TTCAN protocol specification. The formal verification research work described here was conducted in parallel with the preparation of the ISO standard protocol specification for TTCAN.