Model checking based analysis of end-to-end latency in embedded, real-time systems with clock drifts

End-to-end latency of messages is an important design parameter that needs to be within specified bounds for the correct functioning of distributed real-time control systems. In this paper we give a formal definition of end-to-end latency, and use this as the basis for checking whether a stipulated deadline is violated within a bounded time. For unbounded verification, we model the system as a set of communicating Timed Automata, and perform reachability analysis. The proposed method takes into account the drift of clocks which is shown to affect the latency appreciably. The method has been tested on a medium sized automotive example. Categories and Subject Descriptors C.3 [Special-purpose and Application-based Systems]: Real-time and Embedded Systems General Terms Design, Performance, Verification Keywords Task chain, End-to-end latency, Clock drifts, Model checking, Timed Automata

• Type: Conference
• Year: 2008
• Where: DAC
• Authors: Swarup Mohalik, A. C. Rajeev, Manoj G. Dixit, S. Ramesh, P. Vijay Suman, Paritosh K. Pandya, Shengbing Jiang
• Keywords: DAC 2008, Design Automation, End-to-end Latency, Keywords Task Chain, Real-time Control Systems