| 基于扩展Petri网的安全关键软件需求模型检验 |
| |
| 引用本文： | 李震,刘斌,殷永峰,李晓勋.基于扩展Petri网的安全关键软件需求模型检验[J].沈阳工业大学学报,2011,33(1):113-120. |
| |
| 作者姓名： | 李震 刘斌 殷永峰 李晓勋 |
| |
| 作者单位： | 北京航空航天大学可靠性与系统工程学院; |
| |
| 基金项目： | 总装备部“十一五”重点预研项目(51319070101); 航空科学基金资助项目(20095551025); 大飞机总体机载软件工程化研究专题(DY09Z11926) |
| |
| 摘 要： | Petri网是系统建模的形式化方法，为了解决其在软件需求建模和建立程序语义映射方面存在的不足，提出了一种扩展Petri网的方法来支持软件需求建模，区分了状态型和数值型库所，根据软件特点有针对性地扩展了变迁的可触发条件和迁移运算，同时建立了和模型检验程序语言的映射，将扩展Petri网作为检验的模型输入，利用时态逻辑描述运行性质，进行需求模型检验.定时器和航空发动机的防喘功能验证实例结果表明，扩展Petri网可以较好地支持软件系统需求建模和软件程序语义映射，通过模型检验和反例路径分析，可以达到修改和完善需求模型的目的，从而提高软件的质量和安全性.
|
| 关 键 词： | 武器系统 安全关键软件 软件可靠性 软件安全性 软件工程 Petri网 模型检验 形式化验证 |
Requirement model checking of safety-critical software based on expanded Petri net |
| |
| LI Zhen,LIU Bin,YIN Yong-feng,LI Xiao-xun.Requirement model checking of safety-critical software based on expanded Petri net[J].Journal of Shenyang University of Technology,2011,33(1):113-120. |
| |
| Authors: | LI Zhen LIU Bin YIN Yong-feng LI Xiao-xun |
| |
| Affiliation: | LI Zhen,LIU Bin,YIN Yong-feng,LI Xiao-xun(School of Reliability and System Engineering,Beihang University,Beijing 100191,China) |
| |
| Abstract: | Petri Net is a formal method of system modeling.To solve its insufficiencies in software requirement modeling and program semantic mapping,an extended Petri net was proposed to support the software requirement modeling.The state place and numerical value place were distinguished.The triggering condition of transition and the migration operation were pertinently expanded according to the characteristics of the software,and the semantic mapping of model checking program was built.The extended Petri net was re... |
| |
| Keywords: | weapon system safety-critical software software reliability software safety software engineering Petri net model checking formal verification |
| 本文献已被 CNKI 等数据库收录！ |
| 点击此处可从《沈阳工业大学学报》浏览原始摘要信息 |
|
点击此处可从《沈阳工业大学学报》下载全文 |
