摘要：根据权威统计数据,软件测试中发现的70%以上的错误由需求获取或体系结构设计引起.因此,应用软件体系结构在设计阶段的正确性验证非常重要.现有的软件体系结构设计方法不支持需求满足验证,需求满足验证需要其他验证工具的支持.面向主流Web应用软件的体系结构设计及其需求满足验证,提出了一种高阶类型化软件体系结构建模和验证语言(SAML)与软件体系结构建模和验证方法(SAMM).SAML语言通过定义类型和项的语法及语义,描述软件体系结构中类型和对象的构造,通过定义类型规则及其类型检查算法来判定Γ┝t:T和Γ┝R(T1, T2)是否成立.SAMM给出了软件体系结构建模范式,包括构建接口类型Mcls(typeinterface)、组件Mcmpt(component)、容器Mcont(container)、框Mfrm(frame)和框架Mfrwk(framework)这5层建模过程,以及生成层内与层间类型之间关系对应的类型规则,同时定义了接口类型方法调用图(GSA)用以刻画软件体系结构设计要求,定义了类型序列及其正确性用以刻画需求期望的性质,并给出了相应的验证算法.设计实现了基于该方法的原型工具系统SAMVS,其中,模型编辑环境支持应用软件的设计过程,验证环境支持设计满足需求的自动化验证.通过一个实际案例,完成了一个较大规模"互联网+"应用软件系统的体系结构建模和验证.