Extension UML-based Web application formalization modeling and verification method

Abstract

The invention discloses an extension UML-based Web application formalization modeling and verification method, which comprises the following steps: step (1), extracting functional demands of a software system to be designed, and performing demand analysis, step (2), performing UML modeling; step (3), using XML to represent the aforementioned UML2.3 model; step (4), generating formalization description; step (5), performing security attribute verification. The invention provides a feasible method for automatic conversion from the UML2.3 model to the formalization language to expand class diagram, sequence diagram and state diagram in the UML2.3 to implement protocol verification in Web application and implement automatic conversion from the UML model to pi calculation formalization language, and greatly reduces the difficulty of carrying out formalization modelling on the protocol directly; the formalization modeling verification tool is used, and the formalization verification model isrefined; the loophole of the formalization model is detected through display of the verification result and analysis of the attack path, which facilitates quick refining of the model and efficient defect detection.

Description

technical field [0001] This patent relates to the technical field of formalized software requirements analysis, in particular to a formalized modeling and verification method for Web applications combined with the field of formalized analysis and verification of security attributes. Background technique [0002] As the scale of software engineering continues to expand, the complexity of software continues to increase, and software systems are more prone to errors and omissions. In addition, the further the delay in fixing system vulnerabilities throughout the software lifecycle, the more expensive it will be. Therefore, in the early design and modeling stages of software systems, it is of great significance to improve software quality by combining software development methods and formal methods for vulnerability analysis and defect detection to ensure system reliability. [0003] At present, the modeling of formal methods is mainly realized through the analysis of software ...

AI Technical Summary

Problems solved by technology

[0005] However, the present invention aims at the above-mentioned status quo, finds through research and analysis that although combining UML and formalized methods can reduce modeling difficulty and provide formalized semantics and verification for the system, there are still many deficiencies in the existing methods: 1 ) lacks the characteristics of web application-related protocols, and can only model part of the security protocol, and does not propose a system framework for the corresponding domain modeling; 2) usually uses one or two views to model the system, because the view Due to the limitation of selection, when verifying the protocol, there will be a state explosion, and at the same time, the conversion process of the protocol will be very complicated

Images