咨询与建议

看过本文的还看了

相关文献

该作者的其他文献

文献详情 >采用模型检测器的软件安全模型验证方法 收藏

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

A Verification Method of Software Safety Model Based on Model Checker

作     者:陈峰 李伟华 陈昊 吕正 CHEN Feng;LI Weihua;CHEN Hao;L(U) Zheng

作者机构:西北工业大学计算机学院西安710072 西北大学信息科学与技术学院西安710069 

出 版 物:《西安交通大学学报》 (Journal of Xi'an Jiaotong University)

年 卷 期:2011年第45卷第2期

页      面:15-20页

核心收录:

学科分类:08[工学] 0835[工学-软件工程] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术(可授工学、理学学位)] 

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

主  题:软件安全分析 确定有限自动机 形式化建模 模型检测 

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

读者评论 与其他读者分享你的观点

用户名:未登录
我的评分