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.%为了解决Petri网对复杂软件系统进行形式化验证时在安全性描述、自动化程度和验证效率方面存在的不足,提出一种软件安全Petri网.扩展了库所定义,提出了安全距离及其计算方法,以增强Petri网对软件安全性的描述能力.设计了自动划分子网结合库所安全定级的递归算法,仅对与被验证需求性质相关的划分子模型进行验证以提高验证效率,同时实现库所的安全定级.设计并实现了软件安全性需求自动化建模和验证工具原型,最后给出了在典型安全关键软件——机载除冰软件系统上的应用以说明方法和工具原型的有效性.
展开▼
