Structure and behavior preservation by Petri-net-based refinements in system design

A refinement is a transformation for replacing a simple entity of a system with its functional and operational details. In general, the refined system may become incorrect even if the original system is correct because some of its original properties may have been lost or some unneeded properties may have been created. For systems specified in pure ordinary Petri nets, this paper proposes the conditions imposed on several types of refinement under which the following 19 properties will be preserved: state machine, marked graph, free choice net, asymmetric choice net, conservativeness, structural boundedness, consistence, repetitiveness, rank, cluster, rank-cluster-property, coverability by minimal state-machines, siphon, trap, cyclomatic complexity, longest path, boundedness, liveness and reversibility. Such results have significance in three aspects: (1) It releases the designer's burden for having to provide different methods for individual properties. (2) In the literature, refinements have been shown preserving several equivalence relations and behavioral properties. Our results show that they also preserve many structural properties. (3) It greatly enlarges the scope of applicability of refinements because they can now be applied on systems that satisfy more properties than just liveness and boundedness. (C) 2004 Elsevier B.V. All rights reserved.