学位论文 > 优秀研究生学位论文题录展示

基于符号化模型检测的软件演化过程模型验证

作　者: 刘金卓
导　师: 李彤
学　校: 云南大学
专　业: 系统分析与集成
关键词: 软件演化过程模型验证性质验证行为验证 Petri网时序逻辑符号模型检测
分类号: TP311.52
类　型: 博士论文
年　份: 2013年
下　载: 63次
引　用: 0次
阅　读: 论文下载

内容摘要

本论文的研究工作主要包含了以下几个方面：1)提出了软件演化过程模型验证语言CEPDL (Concise Evolution Process Description Language);2)证明了白盒建模软件演化过程模型的结构优良性；3)利用CEPDL语言对软件过程模型进行了动态性质验证；4)构建了软件演化过程模型行为图的行为规约并且利用CEPDL语言对软件演化过程模型进行了行为验证。CEPDL语言是在文献[3]中所提出的软件演化过程元模型EPMM (Software Evolution Process Meta-Model)基础上发展而来的。文献[3]基于基本Petri网,扩展了面向对象技术和Hoare逻辑,提出了EPMM,有效的解决了软件演化过程的形式建模问题,但是,描述EPMM的语言EPDL只能对软件演化过程模型进行描述,不能描述过程模型的性质。CEPDL语言增加了基于线性时序逻辑的性质描述模块,可以充分的描述模型的性质规约,从而使得验证人员能够使用模型检测方法对软件演化过程模型的性质规约进行验证。给出了白盒建模的软件演化过程模型的关联矩阵描述以及细化操作的关联矩阵表示方法。利用关联矩阵证明了通过白盒建模的软件演化过程模型具有有界性、守恒性等等Petri网的经典结构性质。利用CEPDL语言对软件演化过程模型的进行了动态性质验证。传统的性质验证方法只能验证情态与情态之间的动态性质。本文采用了符号化模型检测的方法,提出了新的验证方法,给出了条件间强可达性等描述条件与条件之间的动态性质的定义,并且实现了这些动态性质的验证。利用CEPDL语言对软件演化过程模型进行了行为验证。现有的软件演化过程模型的验证方法缺乏对行为的验证,无法保证过程模型的行为与过程规约一致,代提出了对EPMM手动的行为验证,验证人员需要有强大的理论知识背景,手动的计算出过程模型的行为与规约的一致性,在工业界实现困难,使得其应用受到了很大限制。本文采用符号化模型检测的方法,建立行为图,基于线性时序逻辑对软件演化过程模型的行为进行规约,应用CEPDL模型验证语言对行为图和行为规约进行了描述,完成了软件演化过程的模型验证工具SEPMC(Software EvolutionProcess Model Checking),实现了对软件演化过程模型行为验证的自动化。

全文目录

摘要  4-6
Abstract  6-10
第1章绪论  10-15
  1.1 研究背景  10-12
  1.2 目标  12
  1.3 研究内容  12-13
  1.4 创新点  13-14
  1.5 论文的组织结构  14-15
第2章软件过程验证综述  15-23
  2.1 引言  15-16
  2.2 软件过程验证  16-22
    2.2.1 验证内容  16
    2.2.2 验证方法  16-22
  2.3 小结  22-23
第3章相关研究基础  23-41
  3.1 Petri网  23-25
  3.2 软件演化过程元模型(EPMM)  25-30
  3.3 OBDD  30-35
    3.3.1 OBDD的定义  31-33
    3.3.2 OBDD的性质  33-35
  3.4 线性时序逻辑  35-38
    3.4.1 LTL的语法  35-36
    3.4.2 LTL的语义  36-38
  3.5 自动机理论  38-39
    3.5.1 Buchi自动机(BA)  38-39
    3.5.2 广义Buchi自动机(GBA)  39
  3.6 小结  39-41
第4章软件演化过程模型的验证方法  41-48
  4.1 引言  41-42
  4.2 验证原则  42-43
  4.3 总体思路  43-44
  4.4 验证流程  44-47
  4.5 小结  47-48
第5章软件演化过程模型验证语言及工具  48-64
  5.1 引言  48-49
  5.2 软件演化过程建模  49-55
    5.2.1 软件演化过程模型语言的语法  49-53
    5.2.2 案例研究：一个软件演化过程模型  53-55
  5.3 软件演化过程模型的可达图构建  55-56
  5.4 基于OBDD的软件演化过程可达图存储  56-59
  5.5 生成SMV程序  59-63
  5.6 小结  63-64
第6章软件演化过程模型的结构与动态性质验证  64-83
  6.1 引言  64
  6.2 EPMM建模软件演化过程模型结构性质的探讨  64-75
    6.2.1 软件演化过程模型的关联矩阵  65-68
    6.2.2 软件演化过程模型的结构性质  68-75
  6.3 软件演化过程的动态性质  75-80
    6.3.1 软件演化过程模型的性质验证的思路  75-77
    6.3.2 软件演化过程模型的动态性质  77-80
  6.4 软件演化过程模型动态性质的线性时序逻辑(LTL)描述  80-82
  6.5 小结  82-83
第7章软件演化过程模型的行为验证  83-120
  7.1 引言  83-84
  7.2 行为图的构建  84-103
    7.2.1 顺序块的转化  94-95
    7.2.2 选择块的转化  95-97
    7.2.3 并发块的转化  97-99
    7.2.4 迭代块的转化  99-100
    7.2.5 构建行为图  100-103
  7.3 行为规约  103-114
  7.4 软件演化过程模型行为关系的线性时序逻辑(LTL)描述  114-119
    7.4.1 软件演化过程模型性质的线性时序逻辑描述  114-117
    7.4.2 行为图的构造  117-119
  7.5 小结  119-120
第8章软件演化过程模型验证工具SEPMC的设计与实现  120-127
  8.1 引言  120-121
  8.2 SEPMC的体系结构  121-122
  8.3 SEPMC的设计与实现  122-126
    8.3.1 SEPMC的用例图  122
    8.3.2 SEPMC的类图  122-124
    8.3.3 SEPMC的顺序图  124-126
  8.4 小结  126-127
第9章案例研究  127-142
  9.1 引言  127
  9.2 案例一：进销存系统  127-135
    9.2.1 软件演化过程模型建模  128-130
    9.2.2 软件演化过程模型动态性质验证  130-135
  9.3 案例二：应用程序的移植与开发  135-141
    9.3.1 建立软件演化过程模型的行为图  136-137
    9.3.2 软件演化过程模型行为验证  137-141
  9.4 小结  141-142
第10章总结与展望  142-145
  10.1 总结  142-143
  10.2 未来工作展望  143-145
参考文献  145-149
攻读博士学位期间主持和参与的课题  149-150
攻读博士学位期间发表和录用的论文  150-152
致谢  152

基于符号化模型检测的软件演化过程模型验证

内容摘要

全文目录

相似论文