论文摘要
UML已经是软件建模方面的标准语言,UML状态图描述系统在其生命周期中的动态行为。随着系统规模的扩大和复杂度的提高,UML状态图往往包含设计者所未预料到的隐患,通过模型检查技术对UML状态图进行穷举检验就成为一个重要课题。本文首先对一个UML状态图的子集完成形式化分析,这个子集包含层次、并发等语义,可以满足一般应用需求;形式化分析这个UML状态图的子集及其各元素的语法和语义后,对此状态图子集进行形式化定义;在形式化定义基础上,本文提出对状态图进行模型检查的一种新方法,这个新的方法包括状态图山脉算法和迁移提取算法。状态图山脉算法用在UML状态图转化到中间语言XML过程中,这个算法将UML状态图转化为三维视图,扩展UML状态图中迁移和状态的语义,使状态拥有“层”这个新属性,从而可以根据层来为图中所有状态分类;使迁移拥有“迹”这个新属性,从而可以根据迹将迁移分为平地走、上山、下山与先下山后上山四类,从而根据迁移的类型计算出迁移的进入状态集和退出状态集,最终使UML状态图形式化转化为文本格式的XML文件。迁移提取算法用在XML文件转化到Promela文件过程中,不同于以往提取状态的算法,该算法提取的是迁移,把XML中的迁移块提取并置于Promela文件中的主循环中。由于状态图中的状态具有静止特性,而动态的迁移是状态图动态特征的主要体现,所以提取迁移相比提取状态来说,状态图动态特征更加明显。事件处理方面,本文用一个先入先出的事件队列实现状态图的事件处理,Promela代码中,事件队列模块和迁移模块置于程序主模块中,实现UML状态图run-to-completion步语义。本文实现软件SC2Spin,应用状态图山脉算法、迁移提取算法和事件队列,可以将一个UML状态图转化为Spin的输入语言Promela,用户只要在Promela文件头加入状态图中所使用变量的定义和初始化,就可以直接输入Spin来验证UML状态图的死锁、活锁等错误和时序逻辑公式。
论文目录
摘要ABSTRACT第1章 绪论1.1 研究背景1.1.1 统一建模语言UML1.1.2 UML 状态图1.1.3 模型检查1.1.4 Spin/Promela1.2 模型检查状态图的研究现状1.2.1 国外的研究1.2.2 国内的研究1.3 本课题的研究内容1.4 本文组织结构第2章 形式化分析UML 状态图2.1 统一建模语言UML2.1.1 UML 简介2.1.2 UML 的目标2.1.3 UML 概念范围及分类2.1.4 UML 视图2.2 UML 状态机视图2.2.1 事件2.2.2 状态2.2.3 迁移2.2.4 复合状态2.2.5 伪状态2.3 UML 状态图的形式化2.3.1 UML 状态图的形式化定义2.3.2 操作语义和run-to-completion 步语义2.4 小结第3章 模型检查状态图3.1 模型检查3.2 线性时序逻辑LTL3.3 模型检查工具3.3.1 模型检查工具Spin3.3.2 模型检查工具SMV3.4 模型检查状态图的难点3.5 模型检查状态图的一般方法3.5.1 使用SMV 模型检查RSML3.5.2 使用SMV 模型检查STATEMATE3.5.3 使用 Spin 模型检查 STATEMATE3.5.4 使用Spin 模型检查UML 状态图3.5.5 使用 vUML 模型检查 UML 状态图3.6 小结第4章 UML 状态图模型检查算法4.1 状态图山脉算法4.2 迁移提取算法4.3 转化算法分析4.3.1 迁移冲突问题4.3.2 层次化问题4.3.3 并发问题4.3.4 通信问题4.3.5 步语义问题4.3.6 事件队列的模拟4.3.7 选择 Spin 作为转化目标4.4 小结第5章 SC2Spin 的设计、实现和使用5.1 SC2Spin 的设计5.2 SC2Spin 的实现5.3 SC2Spin 的使用5.4 小结第6章 实验6.1 采用方法一的哲学家就餐问题6.1.1 问题描述6.1.2 SC2Spin 生成的代码分析6.1.3 验证结果6.2 采用方法二的哲学家就餐问题6.2.1 问题描述6.2.2 SC2Spin 生成的代码分析6.2.3 验证结果6.3 采用方法三的哲学家就餐问题6.3.1 问题描述6.3.2 验证结果6.4 囚犯问题6.4.1 问题描述6.4.2 验证结果6.5 小结结论参考文献附录A 攻读学位期间所发表的论文和参加的项目致谢
相关论文文献
标签：模型检查论文; 状态图论文; 状态图山脉算法论文; 迁移提取算法论文;
