基于模型检测的模型驱动式开发系统的设计与实现

论文摘要

本文负责基于模型检测的模型驱动式开发系统中UML序列图中消息交互的验证模块开发,介绍了autoPG1.0版本的设计与开发,实现了从UML序列图到模型检测语言的转换以及对模型的验证。autoPG是一套基于模型检测的UML分析工具,它可对UML中Sequence Diagram进行分析和验证,有着坚实、可靠的理论基础。一个UML的序列图是由对象以及消息构成,通过MagicDraw可以将模型输出为XML格式的文件,通过解析该文件可以获取模型的具体信息。autoPG将分析这个XML文件,获取其中的对象模型并且将其转换为Promela这一模型检测语言,最终通过调用模型检测工具XSPIN进行验证,并提交模型验证的结果。一旦模型被验证为正确,将有助于软件系统的后续开发,对提高软件系统的正确性有重大意义。文文的最后将通过实例介绍如何使用autoPG生成Promela并进行验证这一整个过程。

论文目录

• 摘要
• Abstract
• 第1章 绪论
• 1.1 研究背景
• 1.1.1 研究现状
• 1.1.2 存在的问题
• 1.2 论文工作
• 1.2.1 论文研究工作内容
• 1.2.2 论文研究工作贡献
• 1.3 本文的组织结构
• 第2章 关键技术
• 2.1 模型检测与相关技术
• 2.2 SPIN与Promela
• 2.2.1 SPIN
• 2.2.2 Promela
• 2.3 MagicDraw UML
• 2.4 XML元数据交换（XMI）
• 第3章 MagicDraw输出XML文件的分析与解析
• 3.1 MagicDraw总体介绍
• 3.1.1 关键节点
• 3.1.2 XML文件分析
• 3.2 获取方法
• 3.2.1 示例
• 3.2.2 总结
• 第4章 时序图到Promela的转换规则
• 4.1 概念
• 4.2 基本的时序图
• 4.3 时序图-重复
• 4.4 时序图-综合案例
• 4.5 总结
• 第5章 autoPG的设计与实现
• 5.1 autoPG的介绍
• 5.2 Promela程序架构分析
• 5.3 XML文件解析
• 5.3.1 XML节点获取
• 5.3.2 对象的解析
• 5.4 Promela程序的生成
• 第6章 案例
• 6.1 案例一
• 6.1.1 简介
• 6.1.2 交易过程UML描述
• 6.1.3 autoPG案例验证
• 6.2 案例二—死锁
• 6.2.1 死锁概念
• 6.2.2 临界区调度策略UML描述
• 6.2.3 模型验证
• 第7章 结束语
• 参考文献
• 致谢