| 基于UML和SPIN的软件安全模型验证 |
| |
| 引用本文： | 高晓星,李晓霞,薛冰.基于UML和SPIN的软件安全模型验证[J].长沙大学学报,2013(5):69-71. |
| |
| 作者姓名： | 高晓星 李晓霞 薛冰 |
| |
| 作者单位： | 石家庄经济学院职业技术学院,河北石家庄050031 |
| |
| 摘 要： | 介绍了使用模型验证工具SPIN检测软件设计阶段存在的安全漏洞的方法.用LTL描述安全属性,将软件设计转换为PROMELA.通过一个关注时序安全属性的实际案例,证明了该方法的可行性.
|
| 关 键 词： | 模型验证 软件安全 UML SPIN |
Model Checking of Software Security Based on UML and SPIN |
| |
| GAO Xiaoxing,LI Xiaoxia,XUE Bing.Model Checking of Software Security Based on UML and SPIN[J].Journal of Changsha University,2013(5):69-71. |
| |
| Authors: | GAO Xiaoxing LI Xiaoxia XUE Bing |
| |
| Institution: | (Vocational and Technical College, Shijiazhuang University of Economics, Shijiazhuang Hebei 050031, China) |
| |
| Abstract: | The paper introduces a method of detecting the security vulnerability in the process of design with the model checker SPIN. Security attributes are described with LTL formulae and the software design is converted into PROMELA. The feasibility of the method is proved through a case study. |
| |
| Keywords: | model checking software security UML SPIN |
| 本文献已被 维普 等数据库收录！ |
