Security software formal modeling and verification method based on UML and Z

Abstract

With the continuous expansion of software application range and the frequent occurrence of software security accidents, software security has become the focus of attention. This paper proposes a security software formal modeling and verification method, which uses UML to organize the basic structure of software, and uses Z specification to supply security semantics for UML model in order to support formal model verification. This method can guarantee the security of software design, while reducing the complexity of formal modeling. On this basis, this paper also introduces a website register function as case study and discovers the security flaws in the system design; the effectiveness and practicality of this method is then demonstrated. © 2012 Springer-Verlag Berlin Heidelberg.