基于构件的可补偿服务系统设计研究

随着面向服务计算的应用越来越广泛，服务系统的质量引起了广泛关注，由于服务自身及其环境的复杂性，使得服务系统呈现出可补偿特征，因此，研究可补偿服务系统的设计，对提高服务系统的可靠性与安全性具有重要意义。本项目将首先从可补偿服务系统的特点和可信需求出发，研究可补偿程序的形式语言和精化方法，得到能够反映并发系统典型特征的补偿行为解释语义模型；然后在语义模型基础上，结合基于构件的软件形式建模与设计理论的最新进展，研究基于构件的可补偿服务系统的形式模型和精化方法，支持可补偿服务系统多侧面多层面的设计；进一步以形式建模为基础,结合模型检验、定理证明等技术，研究可补偿服务系统的验证技术；最终建立自动化程度高、与主流软件工程环境相结合的基于构件的可补偿系统的建模与验证工具。本项目的研究能显著提高可补偿服务系统的设计能力，能丰富和发展基于构件的可信设计理论，为提高可补偿服务系统的可靠性提供有力支持。

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