基于形式化方法的软构件接口规范

摘要

软件工程是为解决软件危机而诞生的一门学科，基于构件的软件工程CBSE 提高了软件生产效率和质量，日益成为软件开发的主流范型。构件具有黑盒性质，因此，构件通过接口提供服务，而接口是构件开发人员和组装人员共同遵守的契约。但现今构件的工业标准，如CORBA、EJB、COM等，它们的构件模型和接口定义语言IDL 仅仅规范构件接口的型构，而每种构件模型在实现上都有本身的数据结构和行为的描述，故很难提供一种标准规范来开发和组装这些构件，这也就阻碍了CBSE的发展和构件市场的形成。 针对当前构件接口规范存在以上问题，结合构件的特点和形式化语言的方法，本文提出一种形式化接口的标准规范,该标准规范主要运用形式化B 语言和CSP 即通信顺序进程来规范部分构件接口，以促进接口向更抽象、更强功能的方向发展，从而提高构件的抽象级别和粒度。 本文研究的主要内容包括： 首先，简要论述了形式化理论和方法以及CSP 触发事件的概念，并介绍国内外在软件工程形式化一些研究方法及其研究现状与进展； 其次，介绍了当前软构件及其自身的接口定义语言，包括现有的标准规范，如EJB3.0 规范等等； 然后，研究了构件模型的形式化规范，采用形式化方法严格定义的语法来描述构件模型，并对部分语义做了形式化的规范，给出其一般模型使之适用各类具有不同参数特征的构件； 最后，采用形式化B 语言来规范COM和EJB的接口，并结合对EJB中客户端调用过程进行了标准规范。 考虑到实际市场上的运用，本论文主要集中实现COM和EJB 接口的标准规范。