基于UML和SPIN的软件安全模型验证

Model Checking of Software Security Based on UML and SPIN

介绍了使用模型验证工具SPIN检测软件设计阶段存在的安全漏洞的方法.用LTL描述安全属性,将软件设计转换为PROMELA.通过一个关注时序安全属性的实际案例,证明了该方法的可行性.

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.