Verifying timing synchronization constraints in distributed embedded architectures

Correct functioning of automotive embedded controllers requires hard real-time constraints on a number of system parameters. To avoid costly design iterations, these timing constraints should be verified during the design stage itself. In this paper, we describe a formal verification technique for a class of timing constraints called timing synchronization constraints in the recent adaptation of AUTOSAR standard (WPII-1.2 Timing Subgroup, Release 4.0). These constraints require, unlike the well studied end-to-end latency constraint, simultaneous analysis of multiple task/message chains or multiple data items traversing through a task/message chain. We show that they can be analyzed by model-checking with finite-state monitors. We also demonstrate this method on a case-study from the automotive domain.