基于UML时序图的系统形式模型自动生成研究

摘要

伴着全球信息化飞速发展的步伐，系统形式建模在学术界和工业界的应用越来越普遍，其中系统形式建模方法成为构建安全系统的重要保障之一。统一建模语言是一种能够直观的描述系统模型中行为的可视化语言。虽然统一建模语言在软件设计、开发和测试过程中均起着至关重要的作用，但是由于统一建模语言的可视化图形缺少确切的语义描述。对于设计规范要求苛刻的系统，进行模型验证的时候难度比较大，给设计人员带来了更多的挑战。系统形式模型的自动生成与实现成为亟待解决的热点问题，鉴于此，本文的创新点及主要工作分为如下三个部分：
　　（1）依照系统场景需求的系统模型给出语义描述。系统模型具有Kripke结构，并给出系统形式模型的语义描述。对系统模型的语义描述进行扩展，分别给出半形式化描述系统模型UML时序图和有限状态机的语义描述。通过UML时序图内某一对象的语义描述，引出执行确定有限状态机（Execution Deterministic Finite State Machine，EDFSM）的形式描述。
　　（2）在UML2.0时序图已存在片段的基础上，结合Alt和Neg两种片段提出的一种新的适用于特殊系统场景下的Stop片段，Stop片段用于必要情况下终止系统模型中的事件继续执行。根据UML时序图和执行确定有限状态机的语义描述，提出标准UML时序图及带有单一片段的UML时序图中的某一对象到执行确定有限状态机的算法生成规则。
　　（3）结合UML模型的语义描述和FSP（Finite State Process，FSP）进程代数符号表示，介绍深度优先搜索算法并对其进行改进。基于改进深度优先搜索算法设计并实现 FSP进程代数模型的自动输出，运用 LTSA（Labeled Transition System Analysis）工具达到系统形式模型自动生成的目的。本文选用基本考生网上报名系统作为实例，实现基于改进深度优先搜索算法的系统形式模型的自动生成，运用MCA_ETGBA模型检测工具，验证了系统形式模型生成算法的可行性。
　　系统形式模型的自动生成解决了半形式化建模缺乏语义描述的不足，为规范要求高的系统提供了有效途径。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪 论

1.1 研究背景

1.2 研究现状

1.3 本文的主要工作

1.4 本文的组织结构

第二章 系统模型的形式定义

2.1 系统模型及其语义描述

2.2 UML时序图及其语义描述

2.3 有限状态机及其语义描述

2.4 本章小结

第三章 系统形式模型的生成算法

3.1 标准UML时序图到EDFSM的生成算法

3.2 存在单一片段的时序图到EDFSM的生成算法

3.3 复杂UML时序图到EDFSM生成算法

3.4 实例分析

3.5 本章小结

第四章 系统形式模型的自动生成与验证

4.1 FSP进程代数模型

4.2 系统形式模型自动生成

4.3 系统形式模型的验证

4.4 实例分析

4.5 本章小结

第五章 总结与展望

5.1 总结

5.2 展望

参考文献

致谢

攻读硕士期间发表的论文