Requirement model checking of safety-critical software based on expanded Petri Net

Petri Net is a formal method of system modeling. To solve its insufficiencies in software requirement modeling and program semantic mapping, an extended Petri net was proposed to support the software requirement modeling. The state place and numerical value place were distinguished. The triggering condition of transition and the migration operation were pertinently expanded according to the characteristics of the software, and the semantic mapping of model checking program was built. The extended Petri net was regarded as the model input of checking, and the requirement model was checked through describing the operating character with the temporal logic. The verifying results in the timer and the anti-surge function of aero-engine show that the expanded Petri net can preferably support the software system requirement modeling and software programme semantic mapping. The modification and perfection of requirement model can be attained with the model checking and counterexample analysis, which is beneficial to the improvement in both quality and safety of the software.