| 基于划分软件安全Petri网的需求形式化验证 |
| |
| 引用本文： | 李震,刘斌,苗虹,殷永峰. 基于划分软件安全Petri网的需求形式化验证[J]. 系统工程与电子技术, 2012, 34(9): 1966-1972. DOI: 10.3969/j.issn.1001-506X.2012.09.37 |
| |
| 作者姓名： | 李震 刘斌 苗虹 殷永峰 |
| |
| 作者单位： | 1. 江苏科技大学电子信息学院, 江苏 镇江 212003；2. 北京航空航天大学可靠性与系统工程学院， 北京 100191；3. 江苏科技大学经济管理学院， 江苏 镇江 212003 |
| |
| 基金项目： | 国家自然科学基金，总装备部重点预研课题，航空科学基金，机载软件工程化研究专题，江苏高校优势学科建设工程资助课题 |
| |
| 摘 要： | ![]()
为了解决Petri网对复杂软件系统进行形式化验证时在安全性描述、自动化程度和验证效率方面存在的不足，提出一种软件安全Petri网。扩展了库所定义，提出了安全距离及其计算方法，以增强Petri网对软件安全性的描述能力。设计了自动划分子网结合库所安全定级的递归算法，仅对与被验证需求性质相关的划分子模型进行验证以提高验证效率，同时实现库所的安全定级。设计并实现了软件安全性需求自动化建模和验证工具原型，最后给出了在典型安全关键软件--机载除冰软件系统上的应用以说明方法和工具原型的有效性。
|
| 关 键 词： | 软件工程 软件安全性 Petri网 形式化验证 |
Formalization verification of requirements based on partition of software safety Petri net |
| |
| LI Zhen , LIU Bin , MIAO Hong , YIN Yong-feng. Formalization verification of requirements based on partition of software safety Petri net[J]. System Engineering and Electronics, 2012, 34(9): 1966-1972. DOI: 10.3969/j.issn.1001-506X.2012.09.37 |
| |
| Authors: | LI Zhen LIU Bin MIAO Hong YIN Yong-feng |
| |
| Affiliation: | 1. School of Electronics and Information, Jiangsu University of Science and Technology, Zhenjiang 212003, China；;2. School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China；;3. School of Economics and Management, Jiangsu University of Science and Technology, Zhenjiang 212003, China |
| |
| Abstract: | ![]()
|
| |
| Keywords: | |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《系统工程与电子技术》浏览原始摘要信息 |
|
点击此处可从《系统工程与电子技术》下载全文 |
