Action refinement for true concurrent real time

Abstract

Action refinement is an essential operation in the design of concurrent systems, real-time or not. In this paper, we develop an action refinement technique in a real-time non-interleaving causality-based setting, a timed extension of bundle event structures that allows for urgent interactions to model time-out. A syntactic action refinement operation is presented in a timed process algebra based on the internationally standardised specification language LOTOS. We show: (1) that the behavior of the refined system can be inferred compositionally from the behavior of the original system; (2) from the behaviors of the processes substituted for actions with explicitly represented start-points, that the timed versions of a linear-time equivalence (pomset trace equivalence) and a branching-time equivalence (history-preserving bisimulation equivalence) are both congruences under our refinement; and (3) that the syntactic and semantic action refinements we developed coincide under these equivalence notions with respect to a metric and a CPO (complete partial order) based denotational semantics. Therefore, our refinement operations behave well. They also meet the commonly expected properties.