Model Checking of Software Security Based on UML and SPIN
Gao Xiaoxin · Journal of Changsha University · 2013
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.