软件构件的精化、组合和粘合理论研究

基于构件和对象方法被认为是解决开发大型复杂软件的有效方法，并已经在软件工程中获得巨大成功。然而，基于构件和对象方法缺乏坚实的理论基础，例如，人们还不能完整地定义对象语言的语义；也没能给出UML一个标准的形式语义，虽然UML已经在工业界广泛使用。上述理论缺陷导致构件的理论和方法不支持面向对象设计和实现，而面向对象的理论未提供接口的模型来支持黑箱组合。对象本身不支持组合。为了解决构件和对象系统理论问题，何积丰和刘志明等使用Hoare和何积丰的统一程序理论（UTP）给出构件和对象系统一个语义模型，叫rCOS。rCOS已在国内外获得好评。然而rCOS理论缺乏一个关于构件组合、精化 及协调的完整理论,不能有效地处理粘合代码；rCOS的语义亦不能表达实时等一些非功能性需求等。本项目将重点研究这些问题，从而建立一个构件和对象系统的理论基础。

如何对基于构件和对象的软件开发方法给出坚实的理论基础，是计算机软件理论中的一个重要挑战。本课题深入研究了软件构件的精化、组合和粘合理论。对rCOS模型进行了系统的总结和改进，提出了新的基于交替模拟的构件精化理论，在对开放式系统的形式化开发方面有了很大的创新。我们还提出了构件接口自动机模型，对构件间非阻塞地组合和粘合提供理论依据，并尝试在此模型中扩充实时约束，研究实时构件的组合。另外，我们提出了基于图的面向服务和面向对象程序的分析和验证方法。.在本课题的资助下，我们还进行了其它相关工作的研究，比如混成系统的建模与验证，模型检测与模态逻辑等，取得了阶段性成果。