Journal of Systems Engineering and Electronics ›› 2011, Vol. 33 ›› Issue (2): 458-463.doi: 10.3969/j.issn.1001-506X.2011.02.45
李震, 刘斌, 李小勋, 殷永峰
LI Zhen, LIU Bin, LI Xiao-xun, YIN Yong-feng
摘要:
需求形式化建模和模型检验可以提高安全关键软件的可信性,但在模型描述、调试和解释能力方面存在局限。对使用Petri网支持软件系统建模进行了扩展,设定默认值为零的权函数、利用“非”虚线描述在状态为假和变迁失败情况下的触发,增强阈值条件的描述能力,区分了枚举型和数值型库所,区分了普通迁移和强赋值迁移,并给出了扩展后的形式化定义及其和检验语言的语义映射。最后给出在典型机载软件上的应用,建立了软件需求模型和部分映射代码,对模型进行检验、反例路径分析和需求完善。过程和结果表明该方法可以有效的支持实际的关键安全软件需求建模和验证。
中图分类号: