Based On Uml Behavioral Models In The Form Of Software Vulnerability Detection Methods

With the development of the application of computer technologies, the high reliability of software is more and more important. The formal methods are some precise specification and verification based to the mathematic and logical language. Also these formal methods are important to ensure the high reliability of software. The model checking is a verification technology of the formal methods. The research of model checking theories and the application of this technology are becoming the hot topic in the last few years both at home and abroad. So far there are great successes of the application of model checking in the computer hardware, secure protocol verification and so on.In order to implement the high reliability of software, we should first learn and study software vulnerabilities. In this article, not only the categories of software vulnerabilities are given but also the analysis and definition of special software vulnerability are given. The logical languages are the basic of model checking. In order to master the model checking technology, the Computation Tree Logic (CTL) and the Linear Temporal Logic (LTL) are described. The model checking tool SPIN is selected. Therefore, not only the theory of SPIN is learned but also the input language promela is introduces in detail.There are two main ideas for the application of model checking in verification the software vulnerabilities. One is the model checking in the requirements phase and the other is the model checking in the testing the target codes phase. This topic selects the former and implements the formal verification of the software designing models based on the UML action models. The UML modeling is the main visual modeling methods in the software developments today. The modeling process in other formal methods has problems such as the visual modeling and so on. Thus, the integration of these two modeling methods can effectively reduce the difficulties of verification on the software vulnerabilities.The main study is on the model checking the UML action models in the requirement phases. First, the transform rules from the UML action models to the Extended Hierarchical Automata (EHA) models are described. In order to explain these rules clearly, the transformation processes is implemented with the ATM example. Second, the framework with promela is given to describe the EHA models of some UML active diagram elements. At the same time, the model checking processes with SPIN based on the UML active diagram integrated the dinning philosophers problem are exhibited particularly. Also the verification results of deadlock in this problem are also displayed.