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.