Sciweavers

Share
DAC
2008
ACM

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

9 years 3 months ago
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
Swarup Mohalik, A. C. Rajeev, Manoj G. Dixit, S. R
Added 12 Nov 2009
Updated 12 Nov 2009
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
Comments (0)
books