Software Modeling And Verification Based On Petri Net

As Software is becoming more and more important to people's life, how to ensure reliability and security of software to improve the quality becomes an urgent issue. Although UML is widely used as a modeling tool in software design fields, as a semi-formal language, it lacks accurate description and formal definitions, which is hard to verify the correctness of model. Petri net is not only a graphical modeling tool but also a formal method with strict grammar and semantic definitions. Petri net can be used to model and describe the system effectively, at the same time; it has strong capability of dynamically analyzing concurrency, asynchrony and uncertainty of the system.This paper presents an approach to verify UML state charts from system level. First it transforms UML state chart to Petri net at system level, and then model checks the Petri net model. The approach verifies the dynamic behavior of system by verifying whether the Petri net model satisfies the use case described by collaboration diagram.This paper designs and implements an automatic transform tool from UML model to Petri net. It parses the XMI document of UML to obtain the information of UML model. According to the transform rules, the tool invokes DOM API to implement the automatic transformation from UML model to Petri Net Markup Language (PNML). PNML can be recognized by a Petri net modeling tool called CPN Tools. CPN Tools can edit, analyze and verify Petri nets with visual interface. It can be used to analyze, simulate Petri Net model and verify whether the model satisfies the properties described by ASK-CTL formula.In the end, this paper tests the transform process using Borland Together and CPN Tools, and it verifies the correctness of the system through an instance. The approach presented in this paper integrates the UML modeling process and automatic verification process of the transformed model.