Verification method of security model based on UML and model checking

As the development of security operating system, the formal analysis and verification of the security models has been one of the hottest topics now. A new method to verify the correctness of security models is proposed in this paper based on the study of predecessors' work, which made use of the Unified Modeling Language (UML) and model checking. This approach first used the UML to specify the security model in the form of finite state machine diagrams and the class diagrams, and then translated these UML diagrams to the input language of model checkers. And it used the model checker to verify the model's correctness or the violation of security properties for the last step. The authors demonstrate the violation of confidentiality of the DBLP and SLCF model by the new approach.