徐英娟，侯金奎，2

（1.潍坊学院，山东 潍坊 261061；2.山东大学，山东 济南 250101）

1 引言

模型驱动体系结构（model driven architecture，简称MDA）［1］是国际标准化组织OMG定义的一种基于模型的软件开发框架性标准。目前，许多厂商声称自己的产品支持MDA，如Compuware公司推出的OptimalJ、Interactive Objects公司的ArcStyler、IBM的RSA等。然而，目前这些工具产生的目标代码大多只是静态信息，比如系统的整体框架、类的声明（包括属性和方法的说明），高层模型中的动态逻辑和行为建模部分仍需要开发人员手工实现。MDA的发展离不开强有力的系统建模的支持，因此构建完善的行为建模方法对于完善和发展MDA，进一步提高软件开发效率，显得尤为重要［2］。

形式化方法能够满足行为建模的精确定义、严格证明和逐步求精等要求。形式化方法在局部精确描述动作语义方面有UML无可比拟的优势，因此UML和形式化方法集成建模成为当前软件系统研究的热点。Facon等人最初提出了一种从静态类图向B方法转化的方法［3］，并在此基础上深入探讨了在信息系统和数据库应用领域中使用UML和B的组合建模的思想，并通过UML和B的模型转化为B模型，经过多次精化最终生成代码［4］。Germ'an［5］提出一个具有形式语义和语法的面向对象描述语言Hadze。文献［6］提出了将Object－Z引入MDA的思路。然而MDA和形式化结合的研究还处于初步阶段，如何表示及精化等诸多问题还有待进一步解决。

本文基于系统功能中常用的原子操作，提出了一种形式化的复杂行为描述方法，由此设计并实现了一种复杂行为的模型描述以及代码生成。……