Verification of safety-critical software requirement based on Petri-net model checking

It is very beneficial to apply formal modeling and model checking to improve the dependability of safety-critical software, but there are limitations in model description, debugging and explanation. The extension of Petri-net to model the software system and the default value of weight functions to zero are set up, the fire under false state or failed transition by a "Not" dotted line is described, the ability to describe the condition of threshold is enhanced. This paper differentiates between enumeration place and numeric place, between normal transition and value-assigned transition. The formal definition of extended Petri net and its semantic mapping to verification language are given. Finally, the application in airborne engine software to build the software requirement model and the mapping code for verification, counterexample analysis and improvement are given. The process and result show the methodology can effectively support the safety-critical software requirement modeling and verification in practice.