摘要：根據權威統計數據,軟件測試中發現的70%以上的錯誤由需求獲取或體系結構設計引起.因此,應用軟件體系結構在設計階段的正確性驗證非常重要.現有的軟件體系結構設計方法不支持需求滿足驗證,需求滿足驗證需要其他驗證工具的支持.面向主流Web應用軟件的體系結構設計及其需求滿足驗證,提出了一種高階類型化軟件體系結構建模和驗證語言(SAML)與軟件體系結構建模和驗證方法(SAMM).SAML語言通過定義類型和項的語法及語義,描述軟件體系結構中類型和對象的構造,通過定義類型規則及其類型檢查算法來判定Γ┝t:T和Γ┝R(T1, T2)是否成立.SAMM給出了軟件體系結構建模范式,包括構建接口類型Mcls(typeinterface)、組件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)這5層建模過程,以及生成層內與層間類型之間關系對應的類型規則,同時定義了接口類型方法調用圖(GSA)用以刻畫軟件體系結構設計要求,定義了類型序列及其正確性用以刻畫需求期望的性質,并給出了相應的驗證算法.設計實現了基于該方法的原型工具系統SAMVS,其中,模型編輯環境支持應用軟件的設計過程,驗證環境支持設計滿足需求的自動化驗證.通過一個實際案例,完成了一個較大規模"互聯網+"應用軟件系統的體系結構建模和驗證.