The paper is contributed to study an operator for refinement of actions to be used in the design of concurrent real time systems. The refinement operator replaces actions on a given level of abstraction by more complicated processes on a lower level. We define this operator on a causality based, event-oriented timed model. Then we investigate the interplay of action refinement with abstractions in terms of equivalence notions of the linear time - branching time spectrum for concurrent systems in terms of timed partial orders. As a result, we propose variations of these equivalences with additional timing requirements sufficient for preserving equivalences under refinement. Furthermore, when dealing with particular subclasses of the model under consideration, these additional requirements are not still necessary for preservation of the equivalences under refinement.
Abstract
File
andreeva.pdf240.67 KB
Pages
1-25