实时系统模型检测工具FPTAT的算法与实现

Chapter 1 前言	第1-14页
·概述	第8-9页
·实时系统模型检测	第9-12页
·模型检测主要阶段	第9-10页
·线性时序逻辑和分支时序逻辑	第10页
·状态空间搜索方法	第10-11页
·模型检测工具概述	第11-12页
·作者工作和本文组织	第12-14页
Chapter 2 基本定义	第14-23页
·时间自动机	第14-17页
·有限精度时间自动机	第17-23页
·FPTA定义	第17页
·时钟变量	第17-19页
·FPTA相关概念	第19-20页
·FPTA的操作语义	第20-23页
Chapter 3 活动时钟变量	第23-27页
·活动时钟的引入	第23-24页
·活动时钟求解算法	第24-27页
Chapter 4 符号化方法与SDS结构	第27-32页
·符号化模型检测概述	第27-28页
·SDS结构	第28-32页
Chapter 5 FPTAT工具算法和实现	第32-54页
·FPTAT工具总体框架	第32-33页
·模型和性质输入描述	第33-37页
·SDS结构和状态空间的组织	第37-39页
·主要数据结构	第39-44页
·FPTAT工具中的主要算法	第44-51页
·可达性分析的核心算法	第44-46页
·几个重要函数	第46-51页
·实验	第51-54页
·模型描述	第51-53页
·实验结果	第53-54页
Chapter 6 结论	第54-55页
参考文献	第55-58页
在学期间发表论文	第58-59页
致谢	第59-60页
附录 FPZAT接受语言的语法定义	第60-61页