基于BDDs的离散实时时态逻辑RTCTL*的符号化模型检测及证据生成

摘要

模型检测是公认的一种比较有效的验证系统正确性和可靠性的方法。在一些安全至关重要的领域检测预知系统的响应时间、事件调度的延迟等一系列的参数尤为重要。实际上大部分的实时系统都有自己的有效活动时间，即我们只需要检测其在某段时间内的性能和参数，也就是对离散实时系统的模型检测。因此对离散实时时态逻辑的模型检测便成为课题组要解决的关键问题，Real-Time Temporal Logic RTCTL*从很大程度上扩展了逻辑描述范围，是一种表达力更强的规范描述逻辑，因此对 RTCTL*的研究在形式化验证领域中有着重要的影响和意义。
　　论文的主要研究工作概括如下：
　　1．根据离散实时系统的特征与性质提出并构造了弱公平性约束的有限状态迁移系统 Just Discrete System（JDS)作为计算模型，并对JDS之间的同步并行计算规则进行了详细的定义；
　　2．在 CTL*语法和语义的基础上扩展定义并解释了 RTCTL*的语法和语义，并通过一系列的等式转换添加了一些额外的操作到 RTCTL*中；
　　3．通过将 RTCTL*公式映射为状态公式，把 RTCTL*的符号化模型检测问题转化为 CTL的模型检测问题，并对不同类型的RTCTL*公式在模型检测过程中需要借助的第三者（temporal tester）给出构造方法，提出了基于 BDDs的离散实时时态逻辑 RTCTL*的符号化模型检测算法，并从理论上证明了算法的可靠性和完备性；
　　4．论证了生成反例与产生证据这两个概念的对称性，构造了与上述模型检测算法对应的证据生成算法，并同时证明了算法的正确性。

目录

封面

声明

中文摘要

英文摘要

目录

第1章. 引言

1.1国内外研究动态

1.2论文的组织框架

第2章. 基础知识

2.1二值判定图( Binary Decision Diagrams, BDDs)

2.2计算树逻辑CTL*( The Computation Tree Logic)

第3章. 计算模型

3.1 Just discrete system （ JDS ）

3.2关于JDS 同步计算的定义

第4章. 离散分支时态逻辑RTCTL*

4.1 RTCTL*的语法

4.2 RTCTL*的语义

4.3 RTCTL*的模型检测问题

第5章. 基于BDDs的RTCTL*的符号化模型检测

5.1将RTCTL*公式映射为状态公式

5.2基于BDDs的CTL的符号化模型检测

5.3构造 tester

5.4符号化模型检测E ψ

5.5符号化模型检测任意的RTCTL*公式

第6章. 任意RTCTL*公式的证据生成

6.1证据生成算法

6.2正确性证明

第7章. 结论

7.1研究总结

7.2其他相关工作

参考文献

致谢