A petri net model for system design and refinement

This paper considers the use of Petri nets in the system design process. It proposes a new class of Petri nets called Information Flow Nets (IFNs) which are particularly suitable for performing refinement in the system design. We first define the class of IFNs and describe their behavior and some of their useful properties, such as clean termination. The notion of a "well-behaved IFN" is then defined and a top-down refinement technique is presented which allows us to construct arbitrary sized well-behaved IFNs. The conditions required for the refinement technique to preserve the properties of a well-behaved IFN are derived. We formally prove that a refined IFN N″, obtained by substituting a well-behaved IFN N' in a well-behaved IFN N, is itself well-behaved. The significance of such a technique is that it can be used, in a top-down approach to system design, to build systems that are automatically well-behaved. This in turn helps to avoid the difficulty of analyzing large and complex nets.