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

• 作者: 吕正 李伟华 陈峰 陈昊
• 来源期刊: 西安交通大学学报
• 关键词: 软件安全分析 确定有限自动机 形式化建模 模型检测
• 年，卷（期）: 2011,（2）
• 页码范围: 15-20
• 分类号: TP311
• 语种: 中文

摘要

针对软件开发过程中安全性分析与设计不足的问题,在研究现有软件安全性建模及形式化验证技术的基础上,提出了一种适用于面向对象的软件安全性建模与验证方法.建立软件安全属性的非形式化UML模型,采用安全扩展有限自动机创建其形式化模型,并使用线性时序逻辑描述安全属性,将形式化模型与安全属性共同作为模型检测器的输入,得到模型是否满足性质的验证结果,从而实现了软件安全设计与验证技术的有机结合.实验结果表明,该方法能够在软件设计初期对所涉及的安全性进行有效分析与验证.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	陈峰	西北工业大学计算机学院	83	358	12.0	16.0
3	李伟华	西北工业大学计算机学院	167	1420	17.0	30.0
4	陈昊	西北大学信息科学与技术学院	9	29	3.0	4.0
5	吕正	西北大学信息科学与技术学院	6	19	3.0	4.0