DocumentCode :
3176635
Title :
Model Checking a TTCAN Implementation
Author :
Keating, Daniel ; McInnes, Allan ; Hayes, Michael
Author_Institution :
Univ. of Canterbury Electr. & Comput. Eng., Christchurch, New Zealand
fYear :
2011
fDate :
21-25 March 2011
Firstpage :
387
Lastpage :
396
Abstract :
This paper describes how the SPIN model checker has been applied to find and correct problems in the software design of a distributed vessel control system currently under development at a control systems specialist in New Zealand. The system under development is a mission critical control system used on large marine vessels. Hence, the requirement to study the architecture and verify the implementation of the system. The model checking work reported here focused on analysing the implementation of the Time-Triggered Controller-Area-Network (TTCAN) protocol, as this is used as the backbone for communications between devices and thus is a crucial part of the control system. The starting point was to develop a set of general techniques for model checking TTCAN-like protocols. The techniques developed include modelling the progression of time efficiently in SPIN, TTCAN message transmission, TTCAN error handling, and CAN bus arbitration. These techniques form the basis of a set of models developed to check the implementation of TTCAN in the control system as well as the fault tolerance schemes added to the system. Descriptions of the models and properties developed to check the correctness of the implementation are given, and verification results are presented and discussed. This application of model checking to an industrial design problem has uncovered and corrected a number of potentially costly issues in the original design.
Keywords :
controller area networks; formal specification; formal verification; marine control; marine engineering; safety-critical software; CAN bus arbitration; New Zealand; SPIN model checker; TTCAN error handling; TTCAN message transmission; control systems; distributed vessel control system; industrial design problem; large marine vessels; mission critical control system; model checking; software design; system architecture; time-triggered controller-area-network protocol; Control systems; Open systems; Process control; Protocols; Schedules; Synchronization; Model checking; SPIN; TTCAN; vessel control system;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Software Testing, Verification and Validation (ICST), 2011 IEEE Fourth International Conference on
Conference_Location :
Berlin
Print_ISBN :
978-1-61284-174-8
Electronic_ISBN :
978-0-7695-4342-0
Type :
conf
DOI :
10.1109/ICST.2011.47
Filename :
5770628
Link To Document :
بازگشت