Lee U Jin

The KIPS Transactions:PartD, Vol. 11, No. 1, pp. 115-122, Feb. 2004
10.3745/KIPSTD.2004.11.1.115,   PDF Download:

Abstract

Software system modeling has a goal for finding and solving system´s problems by describing and analyzing system model in formal notations. Petri nets, as graphical formalism, have been used in describing and analyzing the software systems such as parallel systems, real-time system, and protocols. In the analysis of Petri nets, general system properties such as deadlock and liveness are analyzed by the reachability analysis. On the other side, specific properties such as functional requirements and constraints are checked by model-checking. However, since these analysis methods are based on enumeration of all possible states, we propose a new method for mechanically checking system properties with avoiding sate explosion problem. At first, system properties are described in property nets then the system model and the property net are composed and analyzed. In the compositional analysis, system parts irrelevant to the specific property are reduced to minimize the analysis domain of the system. And it is possible to mechanically check whether a specific property is satisfied or not.

Statistics
Cite this article