Structure and behavior preservation by Petri-net-based refinements in system design
Structure and behavior preservation by Petri-net-based refinements in system design
复制标题
DOI：
10.1016/j.tcs.2004.07.016
复制
发表时间：
2004-12
期刊：
影响因子：
--
通讯作者：
Hejiao Huang;T. Cheung;W. M. Mak
中科院分区：
文献类型：
--
作者：
Hejiao Huang;T. Cheung;W. M. Mak
精化是用系统的功能和操作细节替换系统的简单实体的转换。一般来说，即使原始系统是正确的，细化的系统也可能变得不正确，因为它的一些原始属性可能已经丢失，或者一些不需要的属性可能已经被创建。对于纯普通Petri网中指定的系统，本文提出了对几种类型的精化施加的条件，在这些条件下，以下19个性质将被保持：状态机，标记图，自由选择网，非对称选择网，保守性，结构有界性，一致性，重复性，秩，簇，秩簇性质，最小状态机可覆盖性，虹吸，陷阱，圈复杂性，最长路、有界性、活性和可逆性。这些结果有三个方面的意义：（1）它释放了设计者的负担，必须提供不同的方法，为个别性质。(2)在文献中，细化已被证明保留几个等价关系和行为属性。我们的研究结果表明，它们也保持了许多结构特性。(3)它极大地扩大了精化的适用范围，因为它们现在可以应用于满足更多属性的系统，而不仅仅是活性和有界性。
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.