We deal with a distributed time-triggered system consisting of several electronic control units (ECUs). Each ECU contains a processor and a FlexRay-like interface that is connected to a bus. An OSEKtime-like operating system is running on all ECUs. We develop a detailed model of this system and prove its correctness. To do so we formally argue about operating system and driver correctness, termination of applications, and the communication behavior.
Index Terms:
real-time, time-triggered, pervasive, verification, distributed
Citation:
Steffen Knapp, "Pervasive Layered Verification of a Distributed Real-Time System," icons, pp.323-328, Third International Conference on Systems (icons 2008), 2008