随着互联网技术的发展和普及,社会对于软件的形态和开发过程提出了更高的要求,如各种业务应用的快速集成,业务系统的良好适应性及可复用性等。为了满足这种要求,一种面向服务(Service-Oriented)的软件形态正在来临。网络式软件作为一种为了顺应这种新要求而涌现的软件新形态,具有网络化和服务化的特点,集中体现了“软件即服务(Software as a service SaaS)"的核心思想。网络式软件的开发呈现了“用户主导,面向领域,柔性生产”的模式特点,其中,领域的可复用的共性资产是实现网络式软件敏捷开发和满足用户个性化和多元化目标的重要基础。网络式软件的领域建模是构建应用领域可复用的共性资产的过程。O-RGPS元建模框架为网络式软件的领域建模提供了建模视角及其之间的元关系。在元建模框架的指导下,领域建模构建了应用领域中的本体(O)资产,角色(R)资产,目标(G)资产,过程(P)资产,及服务(S)资产。这些不同视角的资产并非完全正交和独立的,而是呈现多层次、多粒度、且在语义层面上相互耦合。为了有利于这些语义丰富且相互耦合的领域资产的复用、规约、分析与管理,提出一个合适的资产组织框架来有效地组织这些不同视角的资产是十分必要的。作为O-RGPS元建模框架的深入性基础研究,本文主要关注于领域资产的组织结构、描述及资产间一致性问题的分析和验证。因此,本文拟解决的科学问题为“基于元建模框架O-RGPS,针对语义丰富且耦合的领域资产,如何有效地组织这些不同视角的领域资产,使其能够被正确的复用和管理”。围绕着该科学问题,本文的贡献主要体现在以下几个方面：(1)基于O-RGPS元建模框架,提出了一个以过程模型为核心的形式化的资产组织框架RGPS-SPM(Semantic Process Model),称之为语义过程模型框架。以过程模型为核心的资产组织方式顺应了当前业务过程模型在面向服务计算和面向服务的软件开发中越来越重要的趋势。以过程模型为基点,组合与其语义上强耦合的角色模型、目标模型等资产,从而结构化和模块化的形成以过程模型为核心的语义上高内聚、低耦合的、更大粒度的可复用的组合模型(称之为语义过程模型)。基于多类型谓词逻辑(Many-sorted Predicate Logic)及并发事务逻辑(Concurrent TRansaction logic, CTR),给出了语义过程模型的形式定义,及其内部的角色模型、目标模型及过程模型的形式定义。(2)给出了语义过程模型的模型语义(Model Semantics),基于该模型语义,定义了语义过程模型的一致性公理。语义过程模型作为以过程模型为核心,封装与过程模型在语义上强耦合的角色模型、目标模型的复合模型,其内部的一致性是实现领域资产正确复用的重要前提。给出了语义过程模型的模型语义。基于该模型语义,定义了语义过程模型关于模型间静态语义的一致性公理。(3)基于语义过程模型的模型语义和形式定义,定义了语义过程模型的形式化规约语言SPML(Semantic Process Modeling Language)。O-RGPS元建模框架为领域资产的建模提供了建模视角和视角之间的元关系。然而当前并没有相应的具有足够描述能力的资产规约语言。基于语义过程模型框架,并借鉴语义Web建模语言WSML(Web Service Modeling Language)和OWL-S的特点,定义了语义过程模型的规约语言SPML,该语言可以对O-RGPS框架中各模型(不包括服务模型)进行规约。(4)基于语义过程模型的模型语义,针对目标模型相对于过程模型的可实现性(Realizable)问题,定义了两类验证问题并提出了相应的验证方法。基于语义过程模型的模型语义,给出了目标模型相对于过程模型的可实现性定义。并给出了目标模型相对过程模型的可实现性判定定理。根据该定理,定义了两类关于目标模型相对于过程模型的可实现性的验证问题,即语义过程模型的约束验证和语义过程模型的能力一致性验证问题。一方面,约束验证是过程模型是否满足数据流和目标模型关于过程执行的时序约束；借助进程代数CSP(Communicating Sequence Processes)及其工具FDR2,提出了语义过程模型的约束验证方法。另一方面,能力一致性验证是过程模型的实际执行能力是否同过程模型的能力模型和目标模型对过程模型的能力期望是否相一致。借助谓词抽象技术(Prediate Abstraction)和可满足性求解工具SAT solver,提出了能力一致性的验证方法。简言之,本文主要是在O-RGPS元建模框架下关于领域资产的组织结构、描述、和一致性分析与验证方面作了一定的贡献,为RGPS元建模框架的更深入应用奠定基础。