基于Object-Z的ReflectiveArchitecture形式化研究

Research on ReflectiveArchitecture Formalism Based on Object-Z

将元信息、元建模、反射和软件体系结构结合起来,提出了一种基于反射机制的软件体系结构重用方法,该方法是一种更通用、更便捷的重用方法;该方法定义并构造了一种在设计阶段支持软件体系结构重用的反射机制RMR-SA。描绘了基于反射机制RMRSA的反射式软件体系结构Reflective Architecture的元级体系结构模型。运用形式规格说明语言Object-Z对元级体系结构模型进行了完整的描述;选取链接模式Link,给出了它的初始化定理及其证明过程,以此为范例证明了被形式化的反射式软件体系结构的正确性。

Banding together meta information,meta modeling,reflection and software architecture,we presented a method of reusing software architecture based on reflection mechanism.It is a more versatile and convenient method.This mothod has defined and constructed a reflection mechanism RMRSA for software architecture reuse at software design phase.This paper described the meta-level architecture model of the reflective software architecture based on RMRSA.Moreover,it formalized the meta-level architecture model using the formal specification language--Object-Z completely.Taking the Link schema as an example,this paper also gave the initial theorem and its testified process,so as to testify the correctness of the formalized reflective software architecture.