| 基于Petri网模型检验的安全关键软件需求验证 |
| |
| 引用本文： | 李震,刘斌,李小勋,殷永峰. 基于Petri网模型检验的安全关键软件需求验证[J]. 系统工程与电子技术, 2011, 33(2): 458-463. DOI: 10.3969/j.issn.1001-506X.2011.02.45 |
| |
| 作者姓名： | 李震 刘斌 李小勋 殷永峰 |
| |
| 作者单位： | 北京航空航天大学可靠性与系统工程学院， 北京 100191 |
| |
| 基金项目： | 总装备部重点预研项目(51319070101); 航空科学基金(20095551025); 机载软件工程化研究专题(DY09Z11926)资助课题 |
| |
| 摘 要： | 需求形式化建模和模型检验可以提高安全关键软件的可信性，但在模型描述、调试和解释能力方面存在局限。对使用Petri网支持软件系统建模进行了扩展，设定默认值为零的权函数、利用“非”虚线描述在状态为假和变迁失败情况下的触发，增强阈值条件的描述能力，区分了枚举型和数值型库所，区分了普通迁移和强赋值迁移，并给出了扩展后的形式化定义及其和检验语言的语义映射。最后给出在典型机载软件上的应用，建立了软件需求模型和部分映射代码，对模型进行检验、反例路径分析和需求完善。过程和结果表明该方法可以有效的支持实际的关键安全软件需求建模和验证。
|
| 关 键 词： | 软件工程 Petri网 模型检验 安全关键软件 形式化方法 |
Verification of safety-critical software requirement based on Petri-net model checking |
| |
| LI Zhen,LIU Bin,LI Xiao-xun,YIN Yong-feng. Verification of safety-critical software requirement based on Petri-net model checking[J]. System Engineering and Electronics, 2011, 33(2): 458-463. DOI: 10.3969/j.issn.1001-506X.2011.02.45 |
| |
| Authors: | LI Zhen LIU Bin LI Xiao-xun YIN Yong-feng |
| |
| Affiliation: | School of Reliability and Systems Engineering, Beihang University, Beijing 100191, China |
| |
| Abstract: | |
| |
| Keywords: | software engineering Petri-net model checking safety-critical software formal method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
| 点击此处可从《系统工程与电子技术》浏览原始摘要信息 |
|
点击此处可从《系统工程与电子技术》下载全文 |
