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.

<p>This thesis project was carried out at Volvo Car Corporation. It is based on an EU project called Locust in which a bio-inspired visual sensor system (the Locust sensor system) for automotive collision avoidance was developed. The Locust sensor system is designed to emulate the collision avoidance functionality of the Locust grasshopper, which is well-known for its extraordinary vision based collision avoidance ability, in particular with regard to its fast reaction times to perceived threats. Volvo Car Corporation is interested in the possibility of using the bio-inspired technology developed in the Locust project to improve its already existing collision avoidance systems. Pedestrian collision avoidance is of high interest, for which the properties of the Locust grasshopper are desirable.</p><p>The purpose of this thesis project is to develop two demonstrator vehicles to test the performance of the Locust sensor system, carry out the testing, and evaluate its usability for Volvo Car Corporation. The first vehicle is a scale 1:5 model car that was originally developed in a thesis project at KTH, and the second a full scale Volvo XC90.</p><p>It was found in the testing that the Locust sensor system is promising for pedestrian collision avoidance applications. The results for detecting other vehicles were also acceptable, but Volvo Car Corporation already has other collision avoidance systems with better performance in this regard. In general the test results were very good for speeds up to about 40 km/h. This indicates that the Locust sensor system would be most usable in a city driving environment, parking lot situations, and for driving in residential areas.</p>

This thesis project was carried out at Volvo Car Corporation. It is based on an EU project called Locust in which a bio-inspired visual sensor system (the Locust sensor system) for automotive collision avoidance was developed. The Locust sensor system is designed to emulate the collision avoidance functionality of the Locust grasshopper, which is well-known for its extraordinary vision based collision avoidance ability, in particular with regard to its fast reaction times to perceived threats. Volvo Car Corporation is interested in the possibility of using the bio-inspired technology developed in the Locust project to improve its already existing collision avoidance systems. Pedestrian collision avoidance is of high interest, for which the properties of the Locust grasshopper are desirable. The purpose of this thesis project is to develop two demonstrator vehicles to test the performance of the Locust sensor system, carry out the testing, and evaluate its usability for Volvo Car Corporation. The first vehicle is a scale 1:5 model car that was originally developed in a thesis project at KTH, and the second a full scale Volvo XC90. It was found in the testing that the Locust sensor system is promising for pedestrian collision avoidance applications. The results for detecting other vehicles were also acceptable, but Volvo Car Corporation already has other collision avoidance systems with better performance in this regard. In general the test results were very good for speeds up to about 40 km/h. This indicates that the Locust sensor system would be most usable in a city driving environment, parking lot situations, and for driving in residential areas.

Time-Triggered Controller Area Network (TTCAN) is a hybrid communication paradigm with combining both time-triggered and event-triggered traffic scheduling. Different from the standard Controller Area Network (CAN), communication in TTCAN is performed according to a pre-computed, fixed (during system run) schedule that is called as TTCAN System Matrix. Thus, communication performance of TTCAN network is directly related to structure of the system matrix, which makes the design of system matrix a crucial process. The study in this thesis consists of the extended work on the development of a systematic approach for system matrix construction. Methods for periodic message scheduling and an approach for aperiodic message scheduling are proposed with the aim of constructing a feasible system matrix, combining three important aspects: message properties, protocol constraints and system performance requirements in terms of designated performance metrics. Also, system matrix design, analyses and performance evaluation are performed on example message sets with the help of two developed software tools.