FORMAL MODELLING OF REAL-TIME EMBEDDED AUTOMOTIVE ARCHITECTURE

Article type: Research Article

Authors: Belarbi, Mostefa

Affiliations: Computer Science Department, Sciences and Science Engineering Faculty, Ibn Khaldoun University of Tiaret, Algeria

Abstract: This paper proposes a formal environment for distributed embedded systems. This approach consists of modelling our embedded system in a hierarchical manner by subdividing it into levels. The first level consists of the modelled application using a task set and the operating system objects (semaphores, mailboxes, watchdogs) which schedule tasks to realise application functions. The second level consists of modelling the hardware components of our embedded system. Our distributed system consists of a network of ECU (Electronic Control Unity) in which like-CAN bus allows ECU to communicate with each other. The communication with the ECU is based on pre-emptive fixed priority scheduling. The Architecture scheme contains an OS layer. This paper suggests an approach based on abstraction to different pieces of architecture, e.g., ECU, OS, application, communicating bus, is suggested. A formal method which allows for interaction between software and hardware elements of the distributed architecture is developed. Based on IF-language, models of all these elements are proposed. The external environment of the distributed systems is also modelled. Observer automata is also suggested to specify architecture properties. These ideas are presented through exploration of an automotive case study.

Keywords: communicating timed automata, distributed system, real-time, verification

Journal: Journal of Integrated Design & Process Science, vol. 13, no. 2, pp. 1-18, 2009