支持MDA的形式化需求至UML状态模型的转换研究

摘要

模型驱动架构（MDA）是一种以模型为核心的软件开发方法。MDA开发过程以需求分析阶段为起点，软件开发人员通过阅读分析非形式化或半形式化的需求规格说明，手工创建平台无关模型（PIM）。随着软件产业的飞速发展，人们对软件自动化程度的要求越来越高，需求与PIM的脱节以及PIM的手工创建方式阻碍了软件自动化发展进程。
　　为了解决需求阶段软件自动化程度不足的问题，本文将MDA与B方法相结合，在MDA需求阶段引入形式化需求描述，提出B方法需求规格说明至一种动态PIM——统一建模语言（UML）状态模型的自动转换方法。UML状态模型有助于开发人员理解B方法需求规格说明，发现需求中的逻辑错误。将平台无关的UML状态模型转换为LabVIEW状态模型等平台相关模型（PSM）后，还能应用到相应平台的状态图编程中，使得基于事件的控制与测试系统的自动化生成成为可能。
　　在研究MDA基本理论、核心标准、元建模方法和模型转换技术的基础上，本文选择基于元模型的模型转换方法作为B需求模型至UML状态模型的转换方法。通过分析状态信息在B方法规格说明中的存在形式和改变方式，本文从最终实现效果的角度提出了B方法规格说明至UML简单状态图和UML复合状态图的一组转换方法。
　　在模型转换实现技术方面，本文首先分析B语言词法规则和语法规则，建立B需求元模型。UML状态元模型则由Eclipse开源项目UML2的元模型改写而成。其次，B方法规格说明由B语言直接撰写而成，无法应用到现有的模型转换技术和工具中，需要设计B语言编译器，将B方法规格说明转换为与B需求元模型一致且能够被现有工具识别的XMI格式。再次，本文为B需求模型和UML状态模型设计了ATL模型转换规则。最后，本文将UML状态模型的存储格式调整为能被UML建模工具UML2Tools识别的格式，实现状态模型的可视化显示和编辑。
　　通过上述研究，本文确立了一种B需求模型至UML状态模型的自动转换方法和实现技术途径。经过规格说明编译、模型转换和模型调整三个步骤，B方法规格说明可被自动转换为可视化的UML状态图。改进后的MDA能够在过程源头提供需求有效性和一致性验证，保证了MDA过程后续阶段输入工件的准确性，MDA过程的优点也可得到良好的保持。自动取款机实例的应用，验证了模型转换方法的正确性和有效性。

目录

封面

中文摘要

英文摘要

目录

1 绪 论

1.1 课题研究背景

1.2 国内外研究现状

1.3 本文的研究内容及意义

1.4 本文的组织结构

2 模型驱动架构理论及技术

2.1 MDA基础理论

2.2 MDA核心标准

2.3 模型转换技术

2.4 MDA软件开发

2.5 本章小结

3 形式化方法理论及技术

3.1 形式化方法基础理论

3.2 抽象机理论与技术

3.3 B方法软件开发过程

3.4 本章小结

4 B方法规格说明至PIM的转换方法研究

4.1 MDA过程与形式化过程相结合

4.2 规格说明中状态的存在形式

4.3 规格说明中状态的改变方式

4.4 简单状态模型转换规则

4.5 复合状态模型转换规则

4.6 本章小结

5 支持MDA的模型转换实现方案

5.1 模型转换技术路线

5.2 需求模型与PIM模型的元模型设计

5.3 获取XMI标准的需求模型

5.4 模型转换规则设计与实现

5.5 目标模型的可视化表示

5.6 本章小结

6 模型转换方法应用研究

6.1 需求格式转换实例

6.2 模型转换规则验证

6.3 目标模型可视化实例

6.4 本章小结

7 总结与展望

7.1 研究工作总结

7.2 后续工作展望

致谢

参考文献

附 录