An Analysis of Concurrent System specification on Petri Nets

This paper proposes a technique that evades the calculative quantity problem encountered in verification of a requirement specification. It is important for a requiremant specification that describes a state transition of service of a communications system or an FA (Factory Automation) system to understand all states that may occur. It is this understanding that prohibits states from developing into bugs in a requiremant specification. However, in trying to search all states, it is not practical, due to the calculative quantity, to generate a state tree. This paper provides a means of over coming that obstacle. Communications system service can by described by HLPN (High level Petri Nets). Our approach examines the fundamental nature of a communications system service. Furthermore, we propose an efficient state generative technique to utilize the fundamental nature which of a communications system service. It is possible for our method to utilize even a system with a dispersion structure other than that of an FA or a transportion system. In addition, calculation of the T-invariant of PN is required for the T-invariant extraction from HLPN. Although the PN calculation poses no problem, the extraction from HLPN is quite difficult. Accordingly, our method exploits the strengths of each specification: after simple calculation with HLPN's small quantity, our verification process exploits the bugs-free environment of HLPN. As a result, the pure, relativery quickly extracted T-invariant is available for generating a state tree.