基于扩展Petri网的除冰软件安全需求建模和验证

Petri网是形式化的系统建模方法,以严格的数学基础来保证系统的正确构建,但在支持复杂软件建模和自动化验证方面存在不足.扩展了Petri网的形式语义,区别定义了状态型和数值型库所,区别定义了变迁的激发和抑制状态,引入了无前置、一元和组合判断规则,同时根据形式化定义将模型自动转换为检验程序实施安全性验证.最后给出了以上方法在典型安全关键软件-除冰系统上的应用,过程和结果表明扩展的模型和方法增强了Petri网对复杂软件系统的建模能力,提高了软件的安全性,从模型到验证代码的自动转换解决了完善模型时人工修改相应代码的工作量和因此而引入人为错误的重复工作量的问题.

Modeling and verification of de-icing software safety requirement based on expanded Petri net

As a formal method, Petri net can ensure the correct construction of system but lacks the ability of modeling complicated system and automatic verification. Firstly, the formal semantics of Petri net was expanded, the place of state and numeric were distinctively defined, the transition state of fired and inhibitory were distinctively defined, the non-precondition, unitary precondition and composite precondition were introduced, and the model was transformed into verification program to implement the safety verification according to formal definitions. And then, the effectiveness of this methodology was illustrated with an application in an aircraft de-icing system which is a typical safety-critical system. The process and result show that the expanded model and methodology enhance the ability of Petri net to model complicated software system, improve the software safety, and the automatic transform from model to codes settle the workload of rewrite corresponding code manually and the meaningless faults introduced by that when the model should be modified.