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

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.