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

面向环境演算系统的模型检测算法的研究

作　者: 高静
导　师: 曹子宁
学　校: 南京航空航天大学
专　业: 计算机应用技术
关键词: 模型检测移动环境演算安全环境演算盒子环境演算空间逻辑
分类号: TP274
类　型: 硕士论文
年　份: 2009年
下　载: 15次
引　用: 0次
阅　读: 论文下载

内容摘要

作为一种很重要的自动验证技术,模型检测已得到广泛研究,取得了丰硕的成果并应用到众多领域,引起学术界、工业界的密切关注。模型检测的一般原理是用状态迁移系统( M )表示系统的行为,用模态逻辑公式(ψ)描述系统的属性。这样“系统是否具有所期望的性质?”就转化为数学问题“状态迁移系统M是否是公式ψ的一个模型?”。因此,模型检测的研究主要围绕在为待测系统建模和采用某种方法正确有效地刻画待测系统的属性这两个方面进行。本文研究的系统主要是用于对广域网和因特网上的计算模型建模的环境演算系统,刻画该系统的属性采用的是模态逻辑中的空间逻辑并结合时态逻辑,分别从进程的结构性质与归约动作两方面进行描述。本文所做的主要工作如下:(1)首先研究了环境演算系统中的移动环境演算、安全环境演算和盒子环境演算,在已有的相关研究的基础上对这三个系统进行纵向的分析与比较,并分别给出了系统模拟与示例。(2)基于对上述三个环境演算的分析,给出了它们对应的面向归约语义的空间逻辑。一方面,该逻辑的静态部分刻画进程的结构,这部分不仅包含了传统的结构算子,而且还引入了新的描述进程前缀动作的逻辑算子。另一方面,该逻辑的动态部分刻画进程的归约动作,即做一步τ-动作后进程满足某些性质,本文不采用进程的行为动作语义,因此逻辑中不必考虑in、out等动作执行的情况。(3)分别为本文研究的模型系统和逻辑系统给出了相应的数据结构表示,并基于模型检测技术的原理来判断模型系统是否具有对应逻辑所描述的相关属性。本文给出了上述三个系统的模型检测算法并对算法的正确性进行了验证。

全文目录

摘要  4-5
Abstract  5-12
第一章绪论  12-24
  1.1 引言  12-14
  1.2 模型检测技术概述  14-17
    1.2.1 模型检测的简要历史  14-15
    1.2.2 模型检测的思想综述  15-16
    1.2.3 与其他检测方法的比较  16-17
  1.3 移动计算与π-演算  17
  1.4 移动计算与环境演算  17-20
    1.4.1 移动计算与移动环境演算  17-19
    1.4.2 安全环境演算  19
    1.4.3 盒子环境演算  19-20
  1.5 模态逻辑概述  20-22
    1.5.1 模态逻辑  20-21
    1.5.2 时态逻辑  21
    1.5.3 空间逻辑  21-22
  1.6 本文的主要内容和组织结构  22-24
第二章移动环境演算系统的模型检测  24-48
  2.1 移动环境演算（MA）  24-31
    2.1.1 Ambients  24-25
    2.1.2 MA 语法相关  25-27
    2.1.3 MA 的操作语义  27-30
      2.1.3.1 MA 的结构同余公理和推理规则  27-28
      2.1.3.2 MA 的归约系统  28-30
    2.1.4 MA 的系统示例  30-31
  2.2 MA 对应的逻辑系统  31-38
    2.2.1 CTL? 和CTL  32-33
    2.2.2 MA 对应逻辑的语法  33-35
    2.2.3 MA 对应逻辑的语义  35-38
  2.3 MA 的模型检测算法  38-47
    2.3.1 MA 进程的数据结构表示  38-39
    2.3.2 MA 对应逻辑的数据结构表示  39-41
    2.3.3 MA 的模型检测算法  41-47
  2.4 本章小结  47-48
第三章安全环境演算系统的模型检测  48-57
  3.1 安全环境演算(SA)  48-52
    3.1.1 SA 的语法  49-50
    3.1.2 SA 的语义  50-51
    3.1.3 SA 的系统示例  51-52
  3.2 SA 对应的逻辑系统  52-53
    3.2.1 SA 对应逻辑的语法  52-53
    3.2.2 SA 对应逻辑的语义  53
  3.3 SA 的模型检测算法  53-56
    3.3.1 SA 进程的数据结构表示  54
    3.3.2 SA 对应逻辑的数据结构表示  54
    3.3.3 SA 的模型检测算法  54-56
  3.4 本章小结  56-57
第四章盒子环境演算系统的模型检测  57-67
  4.1 盒子环境演算（BA）  57-62
    4.1.1 BA 的语法  57-59
    4.1.2 BA 的语义  59-61
    4.1.3 BA 的系统示例  61-62
  4.2 BA 对应的逻辑系统  62-63
    4.2.1 BA 对应逻辑的语法  62-63
    4.2.2 BA 对应逻辑的语义  63
  4.3 BA 的模型检测算法  63-66
    4.3.1 BA 进程的数据结构表示  63-64
    4.3.2 BA 对应逻辑的数据结构表示  64
    4.3.3 BA 的模型检测算法  64-66
  4.4 本章小结  66-67
第五章结束语  67-68
  5.1 本文的总结  67
  5.2 进一步的研究方向  67-68
参考文献  68-72
致谢  72-73
在学期间的研究成果及发表的学术论文  73

相似论文

基于BMC的Web服务失配检测方法研究,TP311.52
基于四方的安全电子商务支付协议研究,TP393.08
安全协议自动化分析系统的设计与实现,TP393.08
Web服务事务协调协议WS-TX的形式化分析与验证,TP393.09
基于UPPAAL的电子商务协议安全性分析,TP393.08
基于模型检测方法的可信软件验证技术研究,TP311.52
网络安全协议的模型检测分析及验证系统,TP393.08
基于程序语义的静态恶意代码检测系统的研究与实现,TP393.08
可重配置硬件系统调度算法的模拟与分析,TN791
时间感知Web服务交互适配技术研究,TP393.09
基于XYZ/ADL的Web服务组合验证研究,TP393.09
基于Color Petri Nets的HMIPv6协议形式化验证研究,TN929.5
基于SVO逻辑的多方不可否认协议的形式化分析与研究,TP393.08
基于行为时序逻辑模型检测的研究与应用,TP311.52
基于时态认知逻辑的Web服务模型检测,TP393.09
模型检测在安全协议验证中的研究与应用,TP393.04
安全协议可视化建模和验证方法的分析与设计,TP393.08
THP事务协调协议的形式化分析与验证,TP311.52
无尺度网络下蠕虫的传播模型与检测技术,TP393.08
基于模型检测的动态协同服务间的一致性验证,TP311.52