Abstract
Keywords Real time systems, Model checking, Timed automata, CAN bus, MAC
Abstract - In the last years the in-car communications play more and more important role in automotive technology. With growing complexity of these systems, it is rather difficult to guarantee their correct behaviour. Therefore it is needed to apply new techniques for their analysis. This article deals with verification of a typical automotive IT equipment based on a distributed system. Such system consists of an application SW (designed by application developer) running under real-time operating system (e.g. OSEK) and using standard broadcast communications based on the Controller Area Network (CAN). The crucial problem is to verify both, the time properties (e.g. message response time) and logic properties (e.g. deadlock) of such complex applications.
Well known Rate Monotonic Scheduling (RMS) can be used to guarantee schedulability, when the application consisting of periodic processes is running on mono-processor with priority based pre-emptive kernel and the processes have their deadlines at the end of their periods. Approach of Tindell and Burns predicts the worst-case latencies for CAN as a direct application of the scheduling theory where the common bus is considered as shared resource. The message worst-case response time is influenced not only by its length but also by the maximal length of one lower priority message since a high priority message cannot interrupt the message that is already transmitted. Moreover due to the priority based bus arbitration method the message worst-case response time is influenced by all higher priority messages, considering their occurrence ratio.
This article presents an alternative approach based on model checking while using timed automata and temporal logics. Using this approach we model parts of the distributed system (application SW, operating system and communication bus) by automata. The automata use synchronization primitives enabling their interconnection; therefore the model complexity grows gradually at a design stage. Product of these automata is further used for checking of desired model properties. Important part of this article is CAN arbitration model composed of several timed automatons: bus automaton and transmitter automaton per each message ID. Verification of the CAN model is compared to the results achieved by Tindell and Burns and it is enlarged to deal with internal structure of the application processes, operating system parameters in ABS case study. Moreover, while using the verification approach, one can verify not only the schedulability, but also rather complex properties linked to logic and timing behaviour of the distributed system. On the other hand, high complexity is a drawback of the model checking approach in contrast to quite straightforward equations of the scheduling theory.