Model Checking Of FlexRay Communication Protocol

Nowadays, the automotive systems mainly adopt electronic control units (ECUs)to realize X-by-wire technology. With the X-by-wire technology, the functionalitieswhich was not able be realized mechanically before are now becoming possible.Generally, ECUs in an automotive system follow communication protocols tocommunicate with each other through one or multiple buses. Since communicationprotocols greatly affect the performance of an automotive system, protocols whichcan support high transmission rate and reliability are demanded. Recently, FlexRaycommunication protocol is considered as the de-facto standard of the automotivecommunication protocol. FlexRay communication protocol supports hightransmission rate up to10Mbs while still keeping the properties of reliability andfault-tolerance. These characteristics make FlexRay especially suitable for safetycritical systems. On the other hand, testing process of automotive systems is reallytime-consuming and complicated. In industry, devices implementing communicationprotocols should be prepared for testing applications implemented on ECUs.Connection between ECUs and protocol devices form a testing environment. Tests areconducted focusing on specific node or data transmission with support of data fromprevious tests. Since higher requirements result complex functionalities and thereforemore ECUs are demanded, and the testing process becomes harder along with largernumber of devices and high financial cost.This thesis proposes a framework for verifying design model of automotivesystems with FlexRay. The framework is based on UPPAAL, with a model checker oftimed automata for modeling the time-related behavior. By using the framework forverifying the design models, developers could have better chances to find bugs at thedesign level with the support of model checking technology. This may lead to areduction of cost of the system development while increasing the quality ofapplications. Similar to the devices-based testing, the UPPAAL framework consists ofa FlexRay model and an application model. The former one represents the FlexRaydevices and the later represents the ECUs where applications are implemented. SinceUPPAAL only provides primitive synchronization using channels, the FlexRay modeland the application model have to be specially handled. The FlexRay model is builtupon the specification with three steps of abstraction:1. The model design verification of applications only requires functionalities of sending and receiving frames to bepresented in the FlexRay model. Therefore, only essential and necessary componentswhich provide the communication functionalities are selected.2. With componentsselected in first step, it is not necessary that the FlexRay model has the full behaviorin sending and receiving frames. Behaviors such as adjustments for error control (i.e.fault tolerance feature) can be skipped.3. Due to the heaviness of the FlexRay modelafter step one and two, further abstraction is conducted in order to reduce the statespace while preserving functionalities implemented. The FlexRay model also providesparameters and interfaces for the communication and access of the application model.The application model only needs to follow these parameters and interfaces tocooperate with the FlexRay model as an automotive system design model. To evaluatethe framework, experiments are conducted as follows:(1) A testing applicationmodels with basic behaviors are introduced for examining the validity of the FlexRaymodel;(2) A simple application is established to verify the response time of thesystem which is tested by using observer model;(3) A simplified adaptive cruisecontrol system is introduced to show the feasibility by using the framework onverifying the practical applications. The results of the experiments prove the validityof the FlexRay model and the feasibility of the framework, respectively. Timingproperties are especially examined and experiences of improving the applicationmodel from checking results are learned.