1.一種基于擴展UML的Web應用形式化建模及驗證方法，其特征在于，該方法包括以下流程：

步驟(1)、提取所要設計的軟件系統的功能性需求，進行需求分析；

步驟(2)、進行UML建模，通過自然語言描述需求以實現建模；或者，對Web應用獨有的特征進行抽取，實現對軟件系統的建模，其中：例圖的建模表示軟件系統中關鍵角色的相應行為，而類圖的建模表示軟件系統中每個主要功能及系統中類之間的關系；通過對UML2.3模型視圖進行擴展，進行詳細建模，從而為自動化轉換做出準備，具體包括：擴展的類圖用于表示軟件系統的類型和靜態行為，擴展的時序圖適用于對軟件系統間消息傳遞進行建模，而擴展的狀態圖對軟件系統中行為對狀態的遷移進行表示；

步驟(3)、使用XML表示上述的UML2.3模型；

步驟(4)、生成形式化描述，該步驟包括兩部分：一部分是對模型的靜態視圖進行映射定義，即定義了類圖中元素到形式化語義之間的映射規則；另一部分是對模型的動態視圖即狀態圖和時序圖進行轉換算法的描述，從而根據轉換規則將模型自動轉換為形式化描述，轉換規則分為兩部分處理，一部分是對UML2.3模型導出為xmi模型，并分析模型的結構和標簽屬性、提取出有用的信息，以樹狀結構保存；另一部分是對關鍵信息通過轉換算法實現重組，將相互關聯的信息拼接為形式化語言；

步驟(5)、進行安全屬性驗證，調用集成的形式化驗證工具，對軟件系統涉及的安全屬性進行驗證。