Specification and verification of real-time embedded systems using time-constrained reactive automata

The authors briefly review the time-constrained reactive automata (TRA) model and its use in the specification and verification of real-time embedded systems. Among its salient features is a fundamental notion of space and time that restricts the expensiveness of the model in a way that allows the specification of only reactive, spontaneous, and causal computation. Using the TRA formalism, there is no conceptual distinction between a system and a property; both are specified as formal objects. This reduces the verification process to that of establishing correspondences-namely preservation and implementation relationships-between such objects