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

A Verification Method of Software Safety Model Based on Model Checker

作　　者：陈峰[1,2] 李伟华[1] 陈昊[2] 吕正[2] 

机构地区：[1]西北工业大学计算机学院,西安710072 [2]西北大学信息科学与技术学院,西安710069

出　　处：《西安交通大学学报》2011年第2期15-20,共6页Journal of Xi'an Jiaotong University

基　　金：国家自然科学基金资助项目(60803150;60803151);国家自然科学基金委员会-广东联合基金重点资助项目(U0835004);国家高技术研究发展计划资助项目(2008AA01Z411);陕西省自然科学基金资助项目(2009jm8012);陕西省教育厅自然科学专项资助项目(09JK736);陕西省科技攻关资助项目(2009k08-04)

摘　　要：针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化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 pro- posed 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.

关 键 词：软件安全分析 确定有限自动机 形式化建模 模型检测 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]