基于抽象状态自动机和π演算的UML动态语义研究

发布时间：2017-10-27 02:10

  本文关键词：基于抽象状态自动机和π演算的UML动态语义研究

  更多相关文章： 统一建模语言 形式化方法 抽象状态自动机 π演算

【摘要】：随着集成电路产业的发展,计算机的硬件性能在近二十年内迅速提高。硬件以及计算机应用领域的不断扩展,使得人们对软件技术提出更多更高的要求。如何改进软件的质量,提高开发效率成为软件产业的重要研究工作。 自90年代面向对象的概念提出以来,由于其可视化、可重用、贴近需求等优点获得了广泛认可,模型也成为沟通用户需求和最终实现的重要桥梁。UML统一并扩展了众多的建模语言,采用丰富的图形作为建模元素。UML的强可读性适用于软件开发的初级阶段,但由于缺乏精确的语义元素,所以在分析、设计和实现时难以建立完整、无二义性的模型,也缺乏必要的精化和验证工具。 形式化方法基于严格的数学和逻辑技术,可以对软件系统进行规约、设计和验证,提高安全性与可靠性。形式化的目的是在系统开发的早期阶段发现并消除不一致、不明确或不完整现象。逻辑精确的语义使开发者与用户形成对需求的一致理解,消除了模糊、不一致；语义的验证自动化,提高了系统的可靠性和效率。然而,由于对设计者提出了数学和逻辑的要求,所以形式化方法在应用领域上存在局限性,很难普及。 理想的软件开发是对可视化建模技术和形式化方法的结合。本文研究UML的动态语义,在保证易读性的基础上,增添必要的语义元素,保证模型的无歧义和可验证性,主要研究成果如下： (1)使用抽象状态自动机对UML活动图进行语义规约。首先定义了活动图的静态语义,分别对动作节点(原子节点)、分支节点、并发节点和活动节点分别给出了语义规约,并递归产生了抽象自动机活动图的规约。随后通过规则对活动图的动态行为,如分支、汇合以及触发捕获事件等行为给出了相应的语义规约。在工作流的循环鉴别器模型中,采用这种方法更为清晰地规约了语义。 (2)使用抽象状态自动机对UML状态图进行语义规约。作为UML中描述行为的重要图形,状态图涵盖了对象在其生命周期内的全部转换形态。本文首先给出了状态图的静态语义,规约了迁移及状态的语义,然后在UML状态图的基础上,给出了扩展的抽象状态自动机模型,提出了基于扩展模型的状态图行为语义。 (3)使用抽象状态自动机对UML顺序图进行语义规约。定义了顺序图中消息和对象的语义规约,随后,针对图形中消息传送条件不明确,时序不清晰的问题,为顺序图的消息传送行为进行了规约。 根据前面给出的状态图和顺序图的语义规约,对电梯实例的UML动态模型进行了语义归约和规则验证,消除了在递归调用中可能出现的死锁和不一致。 (4)提出了UML动态图的π增量精化体系。先给出了π演算对UML动态图的语义规约,将动态图中的各个元素分别映射到π演算的进程和通道；然后规约了动态图的各种动态要素,如状态的不同转换模式、各种消息的传送行为等的语义规约。最后利用弱互模拟关系,定义了顺序图和状态图的行为等价性判别标准；提出了最大弱互模拟集、替换规则,并藉此给出了在精化模型上进行增量一致性检测的方法,电话系统的实例表明,这种方法大大提高了验证的效率。
【关键词】：统一建模语言 形式化方法 抽象状态自动机 π演算
【学位授予单位】：华东理工大学
【学位级别】：博士
【学位授予年份】：2015
【分类号】：TP311.5
【目录】：

• 摘要5-7
• Abstract7-12
• 图表目录12-14
• 第1章 绪论14-27
• 1.1 研究背景14-16
• 1.2 面向对象方法学16-21
• 1.2.1 发展历程16-18
• 1.2.2 主要的面向对象方法18-21
• 1.3 形式化方法21-24
• 1.3.1 软件规约的主要技术21-22
• 1.3.2 形式化方法与半形式化方法的优缺点22-24
• 1.3.3 形式化方法与半形式化方法的结合24
• 1.4 课题主要研究内容24-25
• 1.5 论文组织结构25-27
• 第2章 UML形式化规格说明研究动态27-37
• 2.1 UML建模27-32
• 2.1.1 什么是模型27-28
• 2.1.2 为什么要建模28
• 2.1.3 UML的发展史28-30
• 2.1.4 UML的组成30
• 2.1.5 UML的现状及其优缺点30-32
• 2.1.6 UML模型形式化的要求32
• 2.2 相关的研究工作32-35
• 2.2.1 基于Z的UML形式化33
• 2.2.2 基于B的UML形式化33-34
• 2.2.3 基于VDM的UML形式化34
• 2.2.4 基于逻辑的UML形式化34-35
• 2.2.5 基于网络的UML形式化35
• 2.3 现有工作与本课题的对比35-36
• 2.4 本章小结36-37
• 第3章 抽象状态自动机和π演算37-48
• 3.1 抽象状态自动机方法37-43
• 3.1.1 抽象状态自动机概述37-38
• 3.1.2 抽象状态自动机方法学的优点38-39
• 3.1.3 抽象状态自动机的定义39-43
• 3.2 π演算43-47
• 3.2.1 π演算概述43-44
• 3.2.2 演算的语法44-45
• 3.2.3 结构同余性(Structural Congruence)45-46
• 3.2.4 π演算的行为语义46-47
• 3.3 本章小结47-48
• 第4章 基于抽象状态自动机的UML动态图语义规约48-80
• 4.1 UML语义结构48-49
• 4.2 活动图的抽象状态自动机语义49-60
• 4.2.1 UML活动图概述49-50
• 4.2.2 抽象状态自动机活动图的基本定义50-52
• 4.2.3 抽象状态自动机活动图的语义52-56
• 4.2.4 实例应用56-60
• 4.3 状态图的抽象状态自动机语义60-68
• 4.3.1 状态图的基本元素60-61
• 4.3.2 状态图的静态语义元素61-63
• 4.3.3 状态机的动态语义规约63-68
• 4.4 顺序图的抽象状态自动机语义68-74
• 4.4.1 顺序图形式化的意义68-69
• 4.4.2 顺序图的抽象状态自动机模型语义元素69-70
• 4.4.3 顺序图的抽象状态自动机模型语义规则70-71
• 4.4.4 模型的规约和验证71
• 4.4.5 顺序图抽象状态自动机模型实例71-74
• 4.5 顺序图与状态图的一致性验证实例74-79
• 4.5.1 电梯实例74-76
• 4.5.2 语义规约76-77
• 4.5.3 规则验证77
• 4.5.4 分析与层次树模型77-79
• 4.5.5 结论79
• 4.6 本章小结79-80
• 第5章 基于π演算的UML动态图增量精化验证80-101
• 5.1 模型精化80
• 5.2 为什么采用π演算作为精化工具80-81
• 5.3 UML动态子图的π语义模型81-89
• 5.3.1 状态图的π语义81-85
• 5.3.2 顺序图的π语义85-89
• 5.4 互模拟关系89-94
• 5.4.1 行为等价性89
• 5.4.2 图形中的互模拟89-91
• 5.4.3 强互模拟关系91-92
• 5.4.4 弱互模拟关系92-94
• 5.5 增量精化体系94-99
• 5.5.1 电话系统实例94-98
• 5.5.2 等价性分析98-99
• 5.5.3 结论99
• 5.6 本章小结99-101
• 第6章 结束语101-103
• 6.1 本文的主要研究成果101-102
• 6.2 UML动态图形式化语义的研究展望102-103
• 参考文献103-111
• 致谢111-112
• 攻读博士学位期间完成论文及出版著作112

【参考文献】

中国期刊全文数据库 前2条

1 郭峰;姚淑珍;;基于Petri网的UML状态图的形式化模型[J];北京航空航天大学学报;2007年02期

2 刘晖,李明禄;基于抽象状态机的网格系统设计和分析[J];电子学报;2003年S1期

，

本文编号：1101460