Pervasive Layered Verification of a Distributed Real-Time System

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.