Model Checking Time Triggered CAN Protocols

Model checking is used to aid in the design and verification of complex concurrent systems. An abstracted finite state model of a system and a set of mathematically based correctness properties based on the design specifications are defined. The model checker then performs an exhaustive state space search of the model, checking that the correctness properties hold at each step. This thesis describes how the SPIN model checker has been used to find and correct problems in the software design of a distributed marine 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 its 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 their control system. A model of the ISO TTCAN protocol has been created using the SPIN model checker. This was based on work previously done by Leen and Heffernan modelling the protocol with the UPPAAL model checker [Leen and Heffernan 2002a]. In the process of building the ISO TTCAN model, a set of general techniques were developed 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 then form the basis of a set of models developed to check the sponsoring organisation’s implementation of TTCAN as well as the fault tolerance schemes added to the system. Descriptions of the models and properties developed to check the correctness of the TTCAN implementation are given, and verification results are presented and discussed. This application of model checking to an industrial design problem has been successful in identifying a number of potential issues early in the design phase. In cases where problems are identified, the sequences of events leading to the problems are described, and potential solutions are suggested and modelled to check their effect of the system