Abstract:

To solve the problems that the Petri net is inadequate to the ability of safety description, verification automation and effectiveness in verification of complicated software systems, a software safety Petri net (SSPN) is proposed. With extending the definition of place, the safety distance with its algorithm are proposed to improve the Petri net to describe software safety. The recursive algorithm of automated partition and safety grading is designed to verify the partitioned sub-model related to the property to be checked, which improvs the effectiveness of verification and realizes the safety grading in the same time. Based on those work, the prototype tool of automated modelling and verification of software safety requirements are designed and realized. Finally, the effectiveness of this methodology is illustrated with an application to an airborne deicing system which is a typical safety-critical system.