Formalization And Model Checking Methods Of System Security Model Based On UMLsec

Security Problems caused by design fiaws makes50%of the security problems appeared in the process of software system development. Therefore, however solid the software security program is, it is always very important to do risk analysis of system architecture. Safety risk analysis is a natural method which makes technical problems associated with data considerations. It should be completed in the early stages of the software development life cycle. The results of safety risk analysis and the risk categories also drive the software safety requirements analysis and safety testing.Analysis and modeling of system safety requirements aid to set the process of risk analysis on the early demand layer of software life cycle, which is the best choice of software architecture risk analysis. Methods now existing for analysis and modeling of software safety requirements include: to create a safety assessment and analyze the fault tree; to track the key security needs throughout the whole software life cycle; to add safety standards and measurement based on the software quality models. But there are some differences between the traditional software design model and the methods and models mentioned above. The security model of the system often requires a more strict formal analysis and verification, which makes it necessary to use more strict process management and formal design and analysis method for validation of software safety.To use unified modeling language (UML) for software system modeling is now the most popular modeling method. But as the UML is not a formal language, it is necessary to analyze the feasibility of the model built by UML in a formal way to satisfy the need of some softwares for more strict and safe modeling. On the basis of automata theory, the paper puts forward a formal mechanism to describe the UML view and map it to the Promela model so that the security model established by UML can be formalized, the system security model established by the informal UML language can be described in a more clear and strict way. On the other hand, we use the linear temporal logic language LTL to define the software safety security attributes to make the description more intuitionistic and compatible. With the formalized software security model and the attributes described with the LTL language as the input, we verify the feasibility of the software security model with the popular model checker Spin. We use UML to establish a basic software system model based on the current system design process of customer oriented fan selection software for next development, and linear temporal logic language to define the related system attributes and verify the feasible through the model checking tool Spin. It’s a precise and clear process of achievement, which can describe and check the safety of the software model in a better performance that have been proved in practice. It makes the system security could be verified in the design stage.