Loading...
Modeling and verification of a time-triggered networking protocol
Date
2007
Abstract
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 timetriggered 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.
Supervisor
Description
peer-reviewed
Publisher
IEEE Computer Society
Citation
Proceedings of the International Conference on Networking, International Conference on Systems and International Conference on Mobile Communications and Learning Technologies (ICNICONSMCL’06);
Files
Loading...
2007_leen.pdf
Adobe PDF, 339.23 KB
Keywords
ULRR Identifiers
Funding code
Funding Information
Science Foundation Ireland (SFI)