2007_leen.pdf (339.23 kB)
Modeling and verification of a time-triggered networking protocol
conference contribution
posted on 2012-06-20, 08:56 authored by GABRIEL LEENGABRIEL LEEN, DONAL HEFFERNANDONAL HEFFERNANAnalysis 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.
History
Publication
Proceedings of the International Conference on Networking, International Conference on Systems and International Conference on Mobile Communications and Learning Technologies (ICNICONSMCL’06);Publisher
IEEE Computer SocietyNote
peer-reviewedOther Funding information
SFIRights
“© 2007 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.”Language
EnglishUsage metrics
Categories
No categories selectedLicence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC