An equivalence theorem for the operational and temporal semantics of real-time, concurrent programs

The semantics of formal specification languages provide the foundation for their verification methods. Different semantics give rise to different styles of verification. Previous work on the verification of real-time, concurrent programs includes methods based on operational semantics and those for temporal semantics using timed transition systems. However, the promise of verification methods which combine these views has not previously been investigated. The main contribution of this paper is a proof of the equivalence of the operational and temporal semantics of a general specification language for real-time, concurrent programs. This link between semantics justifies formal methods which utilize both the temporal and operational view. A generic programming language is defined for real-time, concurrent programs and a structured operational semantics for the language. Its temporal semantics is defined by way of a translation into timed transition systems. We also define an operational semantics for timed transition systems and prove this equivalent to their standard temporal semantics. We then have two labelled transition system semantics for programs: one via timed transition systems, and our structured operational semantics for programs. The final step is to prove the bisimilarity of these two labelled transition systems.