基于改进Petri网的可信软件模型验证和测试研究
软件被广泛应用到安全关键领域，这时软件可信性的验证和测试提出了严苛的要求．形式化方法以其严格的数学基础保证软件系统的正确构建．Petri网利用库所和变迁支持异步、并发、分布式系统建模，但是缺少对库所和变迁类型的描述，不能满足软件系统复杂的具体行为特征．模型检验工具具有自动化验证和反例生成功能，但是调试和建模能力不够．文章扩展Petri网以更好的支持软件系统的行为建模和分析，建立模型和验证工具的自动化转化机制，对软件系统进行模型检验，利用反例功能获得失效场景路径，指导测试用倒生成，最后给出了定时器示例和机载发动机款件的典型实例应用．
可信软件模型 Petri网 软件测试 模型检验
李震 刘斌 殷永峰 李晓勋
北京航空航天大学可靠性与系统工程学院,北京 100191
国内会议
合肥
中文
502-507
2010-07-24（万方平台首次上网日期，不代表论文的发表时间）