University of Limerick Institutional Repository

Modeling and verification of a time-triggered networking protocol

DSpace Repository

Show simple item record Leen, Gabriel Heffernan, Donal 2012-06-20T08:56:08Z 2012-06-20T08:56:08Z 2007
dc.identifier.citation Leen,G.(2007) "Modeling and verification of a time-triggered networking protocol " (ICNICONSMCL’06) en_US
dc.description peer-reviewed en_US
dc.description.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. en_US
dc.language.iso eng en_US
dc.publisher IEEE Computer Society en_US
dc.relation.ispartofseries Proceedings of the International Conference on Networking, International Conference on Systems and International Conference on Mobile Communications and Learning Technologies (ICNICONSMCL’06);
dc.rights “© 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.” en_US
dc.subject modelling en_US
dc.subject verification en_US
dc.subject time-triggered en_US
dc.subject protocol en_US
dc.title Modeling and verification of a time-triggered networking protocol en_US
dc.type info:eu-repo/semantics/conferenceObject en_US
dc.type.supercollection all_ul_research en_US
dc.type.supercollection ul_published_reviewed en_US
dc.contributor.sponsor SFI en_US
dc.rights.accessrights info:eu-repo/semantics/openAccess en_US

Files in this item

This item appears in the following Collection(s)

Show simple item record

Search ULIR


My Account