基于划分软件安全Petri网的需求形式化验证

• 作者: 刘斌 李震 殷永峰 苗虹
• 来源期刊: 系统工程与电子技术
• 学科: 工学
• 关键词: 软件工程 软件安全性 Petri网 形式化验证
• 年，卷（期）: 2012,（9）
• 所属期刊栏目: 可靠性
• 页码范围: 1966-1972
• 分类号: TP311.5
• 字数: 5429字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-506X.2012.09.37

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘斌	北京航空航天大学可靠性与系统工程学院	73	669	15.0	23.0
2	苗虹	江苏科技大学经济管理学院	21	68	4.0	7.0
3	李震	江苏科技大学电子信息学院	10	27	2.0	5.0
7	殷永峰	北京航空航天大学可靠性与系统工程学院	22	194	8.0	13.0