网络软件配置于网络环境中,是一种特殊的面向服务计算和超大型复杂软件系统。网络软件的需求工程因为其动态拓扑结构、用户的不确定性及持续增长的需求而面临很多问题。而目前软件需求建模方法对面向服务的计算缺乏足够的支持,无法有效聚集分布在网络中的Web服务资源来提高信息系统的开发效率。与此同时,由于Web服务部署在网络环境中,受环境、平台等情境因素的影响尤其明显,因而以用户为中心、提高用户的体验质量正成为软件系统追逐的核心目标之一。RGPS是武汉大学软件工程重点实验室973项目组提出的网络化软件的统一需求元描述框架。RGPS元建模框架,重点关注情境对需求建模的影响与约束,它包括角色(R)层、目标(G)层、过程(P)层和服务(S)层4个层次。RGPS的4个层次之间具有整体协同的关联:角色承担相应的角色目标,参与者具有偏好的个人目标;过程可以完成功能目标,并可以促进非功能目标的实现;Web服务可以实现过程。面向领域的O-RGPS是利用领域本体(O)为领域的R,G,P,S模型提供语义支持。基于RGPS的需求建模过程从分析需求问题空间的组织结构开始,到生成基于服务的解决方案结束。需求验证是软件需求阶段的一个重要环节,未经验证的需求给项目成功带来较大的需求风险。为支持RGPS需求元模型的Web服务规格说明的验证,用语义Web服务语言OWL-S对RGPS的各层次进行了清晰的描述,并通过Petri网和F-logic对其进行形式化建模,以验证Web服务语义一致性约束。在语义Web服务的OWL-S描述基础上,本文讨论了RGPS元模型框架的语义Web服务组合、动态分析的Petri网方法与静态分析的描述逻辑和F-logic方法。主要贡献和创新如下:(1)提出了一种对RGPS元模型框架各层次的形式化表示和分析方法。对R、G、P、S各层内部的结构以及层间的关联一致性问题进行分析。运用Petri网及F-logic形式化方法对RGPS各层次的需求规格说明进行建模。把所获取的由UML描述的需求通过转换为Web服务本体描述,对RGPS的各层次所获取的需求用领域本体层(O-Net)的领域本体来表示。这样,RGPS所获取各层次需求的验证问题就可以转换为用领域本体层的本体统一表示、然后对O-Net进行形式化建模并加以验证的问题。大大降低了分析的复杂度,提高了效率。(2)在动态模型方面,提出了把OWL-S描述的Web服务应用逻辑映射为PNML表示的Petri网本体模型的方法,然后用Petri网对语义Web服务的复合过程进行建模,并分析了其依赖性与复杂性,给出可达性、活性等相关性质的验证方法。(3)在静态模型方面,提出了一种刻画OWL-S的F-logic形式化方法。设计了一个F-logic模型以便验证OWL-S本体,并把由OWL-S表示的RGPS全局性质和框架映射为F-logic类和公式。并给出了对该模型的一致性、可满足性等性质的验证改进的推导规则和定理,以分析OWL-S的建模范型并对OWL-S支持的任务进行推理。(4)实现了集成静态模型和动态模型检查为一体的辅助验证工具原型。该验证工具能对OWL-S描述的Web服务提供有效的验证支持。它以OWL-S来描述及组合RGPS的Web服务规格说明,将OWL-S文档转换为PNML格式,并以Petri模型为动态验证模型,以Pellet和Flora-2为静态模型推理引擎,实现了模型的形式化工具的分析和验证。上述工作为RGPS元模型框架的服务组合和形式化验证提出了问题描述和求解的具体方法。该模型的验证有效地克服了需求验证过程的复杂性和手工操作,有效地降低项目需求风险。