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

基于Petri网的on-the-fly模型检测

作　者: 王妍妍
导　师: 吴尽昭
学　校: 兰州大学
专　业: 计算机软件与理论
关键词: Petri网线性时序逻辑 Büchi自动机模型检测 on-the-fly
分类号: TP301.1
类　型: 硕士论文
年　份: 2008年
下　载: 178次
引　用: 0次
阅　读: 论文下载

内容摘要

Petri网是一种重要的数学模型,它能够有效地对并发系统进行描述和建模。线性时序逻辑LTL则是描述和验证并发系统特性的一种重要的形式化工具,它能够方便、准确地描述并发系统的重要性质,如安全性和活性。自动机理论在模型检测中起着非常重要的作用,模型检测是时序逻辑和自动机理论的有机结合,是关于系统性质验证的算法和方法,它通常采用搜索状态空间的方法来检测一个给定的系统模型是否满足某个用时序逻辑公式表示的特定性质。系统模型的状态空间爆炸问题就是模型检测所面临的主要问题。本文详细地描述了Petri网、线性时序逻辑、Büchi自动机、Petri网的可达图和自动机的交自动机,并详细探讨了在基于线性时序逻辑和自动机理论的Petri网的可达图的模型检测策略的基础上,引入了on-the-fly技术来进行Petri网的模型检测。在on-the-fly模型检测中,事先仅需要构造被验证性质对应的自动机和系统的Petri网模型,在对状态空间的搜索中按照双DFS算法的需要动态地构造Petri网的状态可达图和性质自动机的交自动机,与此同时,利用性质自动机来引导Petri网的状态可达图进行动态地构造。这样,在找到被验证性质的一个反例之前,可能仅需要构造交自动机和状态可达图的部分甚至是一小部分的状态空间,从而避免了对交自动机的整个状态空间的穷尽搜索,来尽可能地减少搜索的状态空间,以此来减缓状态空间爆炸的问题。并且存储Petri网模型的可达图以及可达图和性质自动机的交自动机所占用的空间也会减少,从而也可以很好地缓解内存不足的问题。

全文目录

摘要  4-5
Abstract  5-9
第1章绪论  9-16
  1.1 引言  9-10
  1.2 模型检测  10-14
    1.2.1 模型检测产生的背景  10-11
    1.2.2 模型检测概述  11-14
  1.3 研究内容与本文组织  14-16
第2章 Petri网及其可达图  16-23
  2.1 Petri网的直观理解  16-17
  2.2 Petri网的形式化描述  17-20
    2.2.1 网及其图形表示  17
    2.2.2 P/T系统及其相关定义  17-20
  2.3 抑制弧Petri网  20-21
  2.4 Petri网的可达图  21-23
第3章线性时序逻辑与自动机理论  23-35
  3.1 线性时序逻辑LTL  23-26
    3.1.1 LTL的语法  24
    3.1.2 LTL的语义  24-26
    3.1.3 LTL公式的NNF形式  26
  3.2 自动机理论  26-29
    3.2.1 Büichi自动机  26-27
    3.2.2 泛Büchi自动机  27-28
    3.2.3 标记的泛Büchi自动机  28-29
  3.3 LTL公式到自动机的转换  29-33
    3.3.1 数据结构  29-30
    3.3.2 LTL转换为自动机  30-33
  3.4 交自动机  33-35
    3.4.1 交自动机的定义  33-34
    3.4.2 交自动机的构造算法  34-35
第4章 on-the-fly模型检测  35-43
  4.1 模型检测的步骤  35-37
  4.2 基于自动机的模型检测  37-39
    4.2.1 基于Petri网的自动机模型检测  37-39
  4.3 双DFS算法  39-40
  4.4 on-the-fly模型检测  40-43
    4.4.1 on-the-fly模型检测概述  40-41
    4.4.2 基于Petri网的on-the-fly模型检测  41-43
第5章实例分析  43-51
  5.1 互斥算法  43
  5.2 实例的Petri网模型  43-44
  5.3 实例并发特性的描述  44-45
  5.4 性质LTL公式转换到自动机  45-46
  5.5 用自动机进行模型检测  46-48
  5.6 采用on-the-fly技术进行模型检测  48-51
第6章总结与展望  51-53
参考文献  53-56
在学期间发表的学术论文  56-57
致谢  57

基于Petri网的on-the-fly模型检测

内容摘要

全文目录

相似论文