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

摘要：

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

关键词：软件安全性、软件工程、Petri网、模型检验

所属期刊栏目：38

分类号：TP311.5;N941.5(计算技术、计算机技术)

资助基金：十一五"重点预研课题;航空科学基金;国家自然科学基金;机载软件工程化研究专题

在线出版日期：2012-04-28（万方平台首次上网日期，不代表论文的发表时间）

页码：64-68,105