由于面向服务系统处于开放的环境中，其本身的分布性、动态性和异构性等特点决定了此类软件开发的复杂度会大大提高，为了保证服务系统的可信，人们已开始注重对服务系统在设计阶段的形式建模和验证的相关理论与技术进行研究。从目前看，对于可补偿服务系统，符合其特点的形式模型、验证框架和算法以及有效的建模验证支持工具都有待于进一步研究。对此，本项目提出支持典型并发特征的可补偿形式语言，并对其理论基础和关键技术进行了深入研究。本项目的主要研究成果包括：. （1）在现有可补偿形式语言cCSP的基础上，提出了支持非确定性、死锁和活锁建模的扩展可补偿形式建模语言，解决了递归可补偿进程指称语义解释开问题，定义了可补偿进程的精化关系，为可补偿服务系统的设计提供良好的理论基础。. （2）给出了扩展可补偿形式语言的操作语义，解决了之前语言操作语义的规则不完全问题，并证明指称语义与操作语义之间的一致性，为可补偿服务系统的分析与验证奠定了理论基础。. （3）在扩展可补偿形式语言理论研究的基础上，研究了相应的推理规则，给出了支持精化和死锁推理的部分代数规则；同时研究了扩展可补偿形式语言的正规性质模型检验问题，证明了问题在理论上是不可判定的。. （4）为了支持基于构件的面向服务系统建模与分析，研究提出了基于自动机的构件模型，支持构件内部动作的规约，以及构件相容性和精化的检查；同时，基于现有失败语义模型，提出了基于自动机构件的指称语义失败模型，使构件相容性和精化的检查更容易理解。. 本项目根据上述研究成果设计实现了基于构件的服务系统模型驱动开发支撑工具原型，以及可补偿服务系统的形式建模与模型检验工具原型，并对典型的面向服务软件系统进行了实验验证，取得良好的效果。