Scalable model-checking for precise end-to-end latency computation

Autor: S. Ramesh, Devesh B. Chokshi, Swarup Kumar Mohalik, Manoj G. Dixit, A. C. Rajeev
Rok vydání: 2013
Předmět:
Zdroj: CACSD
DOI: 10.1109/cacsd.2013.6663476
Popis: Correct functionality of automotive embedded control systems often requires that the end-to-end latencies of data items traversing through specified task/message chains from sensors to actuators are within specified bounds. Hence, accurate estimation of the worst-case end-to-end latency has significant impact on the design of system architectures. Model-checking based techniques can provide accurate estimates of worst-case end-to-end latency, as they are based on exhaustive state-space exploration. However, state-space explosion may limit their applicability to small and medium sized systems. In this paper, we present an abstract system model that can be used for model-checking based latency computation, leading to a major increase in scalability. This is achieved by on-the-fly generation of abstract models for task activations, based on a proposed variant of the Joseph-Pandya equation.
Databáze: OpenAIRE