Verifying temporal constraints on data in multi-rate transactions using timed automata

Transactions involving multiple tasks, possibly with different period times, are common constructs used in the design of real-time systems. Data flowing through a transaction is usually subject to temporal constraints, such as maximum time from input to output or a maximum time difference between inputs. Such constraints are of great importance to guarantee the correct functioning of the designed system, but normally they cannot be checked using the traditional approach to schedulability analysis. We describe how to use timed automata and reachability analysis to verify such temporal constraints on data in transactions. By making a timed automaton model of the data dependencies in a transaction, we enable automatic verification of timing constraints such as end-to-end latency. The model can handle different computational models and any non-preemptive execution order of the tasks in the transaction. Our experiences from industrial case studies indicate that in a substantial number of applications, the transactions are of sizes that can be handled using this approach.