In: Burkhard, H.-D.; Czaja, L.; Skowron, A.; Starke, P.: Report No. 140: Proceedings of the workhop on Concurrency, Specification and Programming, Oct 9-11, 2000, pages 213-224. Berlin: Humboldt-University, 2000.
Abstract: Consider a single action of a distributed system which is replaced by a more complex subsystem. In this paper, we investigate conditions which ensure, that the action and the new subsystem behave similar with respect to their environment. The most important condition is, that there are the same causal dependencies between the action and the environment as between the new subsystem and the environment. We use partial order semantics to express this causal dependencies and we suggest a new notion of behavior preserving transition refinement based on partial order semantics. Furthermore, we discuss how to prove the correctness of a transition refinement step. Our results are formalized in the setting of Petri nets. We use Petri nets because they have a canonical partial order semantics, which is defined by concurrent runs.