基于改进Petri网的可信软件模型验证和测试研究

摘要

软件被广泛应用到安全关键领域，这时软件可信性的验证和测试提出了严苛的要求．形式化方法以其严格的数学基础保证软件系统的正确构建．Petri网利用库所和变迁支持异步、并发、分布式系统建模，但是缺少对库所和变迁类型的描述，不能满足软件系统复杂的具体行为特征．模型检验工具具有自动化验证和反例生成功能，但是调试和建模能力不够．文章扩展Petri网以更好的支持软件系统的行为建模和分析，建立模型和验证工具的自动化转化机制，对软件系统进行模型检验，利用反例功能获得失效场景路径，指导测试用倒生成，最后给出了定时器示例和机载发动机款件的典型实例应用．