The Research On Methods Of Formal Software Developing Based On Petri Nets

With the rapid progress of computer software, how to improve the efficiency of software development has become a very important issue. The adoption of formal software technology, which benefits to the intercommunion of developers and promotes the software robustness, not only can decrease great number of errors in the early phase of design, but also reduce the total time of development. Formulation is strictly based on mathematics. By strict verification and analysis, vague and incomplete properties can be found in the course of designing and developing, so as to approach the effective control over software quality, development cost and development progress. Formulation is divided into two parts: formal specification instruction and formal verification. Petri Nets is a perfect description tool meets the two demands listed above.Petri Nets is a tool of description and analysis formulated and graphically for system software, which is intuitive, understandable and User-friendly and so forth. The systems model, which is concurrent, asynchronous, parallel, uncertain and random, can be constructed by this tool. Then, static structure and dynamic behaviors of the system model can be analyzed and gained .According to the information, the system can be appraised and promoted. At the same time, Petri Nets provides a powerful medium for intercommunion in porogramers and formulizes the course of software development.The subject of this paper is the research into methods of formal software developing based on Petri Nets. Mainly consists of simulation and verification. Obtained some new results from deep and comprehensive research on Petri Nets of it's simulation capability and main characteristics, taking advantage of invariable technology, structure analyzing technology and partition modeling technology. Main contributions are:(1)The concurrence control of DBMS is widely paid attention by people in the field all the time, which is a vital criteria of DBMS performance. Moreover, S-invariable as an important verification method of Petri Nets is also increasingly considered by people. Classic S-invariable method usually used for explanation and estimation of system property, or as a kind of qualitative and quantitative analysis of some concrete examples. This paper employs extended Petri Nets to constructe a common DBMS model with locking mechanism, supplies a methodology of formal software development, simulates a DBMS as a whole, and verify the model using S-invariable.(2)At present, most software systems are concurrence. Petri as a good formal description and analysis tool, has to describe and analyze the system very well. Streetlights fault detection system is a concurrence system, in which system signal is transmitted concurrently between the system and streetlights equipments. The paper constructed a kind of system using cyber net with inhibitor or permissive arcs, which adopted formal method of Petri Nets to describe, analyze and verify the system in order to ensure the system's validity. It can be regarded as the research on this issue as an application of Petri Nets.(3)Traffic signal control is an international issue and is a typical concurrence and synchronization system. The paper constructed a kind of traffic signal control system, which facilitates the realization of regional control, with interrupt handling features. The method of block modeling in the modeling process just accords with the modularization principle and object-oriented-design ideology. The accuracy of the model has been analyzed from the structure definition of a sequence in the nets.