论文部分内容阅读
基于构件的模型驱动开发被认为是实现软件复用和降低系统开发复杂度的重要技术之一,并已在工业界得到广泛应用。其基本思想是:根据不同的视角和关注点将系统分解为不同模型,然后从较高层次、平台独立的抽象模型开始,经过一系列模型转换,转换为较低层次、平台相关的具体模型,直至生成代码。
构件模型之间的精化关系在模型驱动开发中扮演关键角色,它刻画了构件之间的可替代关系,为构件模型转换规则提供了语义基础。以往工作中构件模型的精化关系一般定义为系统行为之间的包含关系,即一个系统精化后,其行为构成的集合被精化前行为构成的集合所包含。从构件设计和开发的角度看,这种精化关系仅仅考虑到模型安全性质的保持,无法体现一个构件精化后应该对外界环境更易反应这样的直观感觉,因此不适合于构件之间的比较。本文在构件模型之间提出了新的精化关系,一个构件是另一个构件的精化,则意味着它提供更好的服务,并且对外界环境具有更强的反应能力。该想法与Alur、Henzinger等学者在研究开放系统及其逻辑中形成的观点一致。他们将开放系统定义为一个基于博弈论的多代理系统,精化关系定义为交替精化关系,一般由交替模拟实现。本文证明了新定义的精化关系是一种交替模拟关系,而构件显然是一种开放系统,这就从理论上表明了本文定义的合理性。
本文的工作基于rCOS构件模型。rCOS是何积丰和刘志明等提出的一个基于构件的集成形式化开发方法,为不同抽象层次的构件模型提供了基于共同语义理论的建模符号和语义表示,包括构件接口、合同、实现、规约、发布等。本文具体工作和创新如下:
1.本文在构件合同模型中提出了一种全局精化关系,称为迹精化关系,在这种精化关系下,一个构件合同精化后,从静态功能看,会提供更好的服务,从与环境交互行为看,会提供更多服务。本文还提出了一个更易于验证的局部精化关系,称为数据精化关系,并证明了它可以蕴含全局精化关系。
本文证明了新定义的精化关系是一种交替模拟关系,从理论上表明定义的合理性。
2.本文提出了一种比较接口相异的合同的方法,思想是通过定义在合同上的内部化算子将合同之间的不同方法内部化,然后使用定义的精化关系对接口相异的合同进行比较。这样做有效克服了原始交替模拟关系中的副作用,并且弥补了传统精化方法只适合于比较接口相同的合同的局限。
3.本文进而将构件合同模型上定义的精化关系扩展至构件的实现模型,并定义了组合操作算子。在构件实现模型定义了构件实现的语义函数,于是构件实现之间的精化关系定义为语义函数计算得到的供应合同之间的精化关系。本文还证明了定义的组合操作算子对于该精化关系是单调的,这表明可以通过精化单独的构件对整个系统进行精化,因而支持了基于关注分离的开发。
4.本文最后定义了构件规约模型之间的交替精化关系,并定义了规约上的组合操作算子。在构件规约模型定义的精化关系,使得规约在精化后提供更好和更多的服务,而需要更弱和更少的服务。本文证明了这依然是一种交替模拟关系,说明了其合理性。本文进而证明了定义的组合操作算子对于该精化关系是单调的,从而支持了基于关注分离的开发。