采用模型检测器的软件安全模型验证方法

摘要

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.%In order to improve the analysis and design of software safety, on the basis of current researches on safety model and verification technology, a modeling and checking method is proposed for object-oriented software safety.Establishing non-formal UML models of software safety, safety extended deterministic finite automata and linear temporal logic are used to create the formal models and describe the safety properties separately.Through a model checker, we get the verification result.This approach realizes the combination of software safety model and verification technology.Experimental results show that the method can analyze and verify the safety properties effectively in the early stage of software design.