| Abstract: | A safety-critical system needs fault-tolerant communication between its components. This is especially important for automotive domain, as it consists of distributed real-time systems that are based on the results of the communication. To realize distributed systems with predictable time behavior the time-triggered paradigm is used. According to this paradigm, a time-triggered communication protocol, FlexRay, and an operating system OSEKtime with corresponding communication layer FTCom for the fault-tolerant communication are introduced. In this paper we present the formal specifications of FlexRay and FTCom that allow us to argue about their properties in a precise, formal manner and also infer the collaboration between their properties. |
