Action Refinement for Real-Time Concurrent Processes with Urgency

We propose an action refinement approach for real-time concurrent processes with urgent interactions, where a partial-order setting, timed bundle event structures, is used as the system model and a real-time LOTOS-like process algebra is used as the specification language. We show that the refinement approach has the commonly expected properties: (1) The behaviour of the refined process can be inferred compositionally from the behaviour of the original process and from the behaviour of the processes substituted for actions; (2) The timed extensions of pomset trace equivalence and history preserving bisimulation equivalence are both congruences under the refinement; (3) The syntactic and semantic refinements coincide up to the aforementioned equivalence relations with respect to a cpo-based denotational semantics.