时间区间时序逻辑模型检测：理论、算法及应用
发布时间：2023-02-10 08:50
行为、事件具有实时关系的软件或硬件系统构成了实时(计算)系统。在交通控制,航空航天等一系列对安全性要求极高的应用领域,实时系统的形式化验证成为保证系统正确性的重要手段。实时模型检测就是其中的一类自动验证方法,原理是实时逻辑公式描述系统所需满足的性质,时间自动机建立系统模型,验证算法自动判定模型是否满足性质。实时逻辑有很多种,用于形式化描述与验证也各有其优势,时间区间时序逻辑就是其中的一种线性实时逻辑,并已被应用于对一些实时系统的形式化描述与分析中。虽然该逻辑有其独特的比较优势,然而到目前为止,时间区间时序逻辑还不能用于实时系统的模型检测,因为缺少验证方法,也没有支撑方法的形式化理论来加深人们对该逻辑的理解和认识。针对于此,本文研究命题部分的时间区间时序逻辑模型检测问题,以该问题为主线,从理论、方法、应用三个层面构建其体系。 为了搞清楚该逻辑可以描述哪些性质、是否可应用于模型检测以及模型检测的效率,本文分别从逻辑的表达能力、判定性及复杂性三个方面进行研究,从而形成该逻辑模型检测的形式化理论。证明了离散时间域上的该逻辑与离散时间正则表达式、离散时间自动机等价,结果表明一切离散时间正则语言均...
【文章页数】：146 页
【学位级别】：博士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 研究背景与研究现状
1.1.1 模型检测
1.1.2 区间时序逻辑
1.1.3 实时系统模型检测
1.1.4 时段演算
1.1.5 基于模型检测的入侵检测
1.2 存在的问题及本文工作
1.3 论文组织结构
第二章 时序逻辑
2.1 命题投影时序逻辑
2.1.1、语法
2.1.2、语义
2.1.3、导出公式
2.2 命题区间时序逻辑
2.2.1、语法
2.2.2 语义
2.2.3 导出公式
2.3 正则图算法与满足性判定
2.3.1 正则形
2.3.2 正则图
2.4 复杂度分析
2.5 chop star 公式的满足性判定
2.5.1 扩展命题区间时序逻辑EPITL
2.5.2 EPITL 可满足性判定
2.5.3 EPITL 可满足性判定问题固有复杂度与算法复杂度
2.6 小结
第三章 实时逻辑与自动机
3.1 时间区间时序逻辑
dense-R"> 3.1.1 实界稠密时间区间时序逻辑TITL<sub>dense-R
dense-N"> 3.1.2 整界稠密时间区间时序逻辑TITL<sub>dense-N
3.1.3 实样本时间区间时序逻辑TITLsample-R
3.1.4 整样本时间区间时序逻辑TITLsample-N
3.1.5 TITL<sub>dense-R 、TITL<sub>dense-N 、TITLsample-R 和TITLsample-N 的关系
3.2 时间自动机
3.2.1、稠密时间自动机
3.2.2、离散时间自动机
3.3 时间正则表达式
3.3.1、有穷时间
3.3.2、无穷时间
3.4 离散时段演算
3.5 小结
第四章 TITL 公式可满足性判定
4.1 TITLN公式可满足性的判定问题
4.1.1 时间正则图
4.1.2 TITLN公式可满足性判定算法
4.1.3 两个例子
4.1.4 复杂度分析
4.1.5 相关工作比较
4.2 TITLR公式可满足性的判定问题
4.2.1 TITLR公式可满足性的不可判定性
4.2.2 有关TITLR公式判定性与复杂性结论
4.3 小结
第五章 TITL 模型检测
5.1 离散TITL 模型检测
5.2 稠密TITL 模型检测
5.3 相关工作比较
5.3.1 基于非时间化的TITLN判定算法的抽象描述与分析
5.3.2 两种方法比较
5.4 小结
第六章 离散TITL 表达能力
6.1 TITLN
*
6.1.1 语法
6.1.2 语义
6.2 TITLN
*→TAN
6.3 TAN→TREN
6.4 TREN→TITLN
*
6.5 TITLN
*、TAN、TREN的等价性定理
6.6 TITLN与{┌w┐,l=k}-DCN}的等价定理
6.7 小结
第七章 统一逻辑框架模型检测
7.1 命题投影时序逻辑统一模型检测
7.1.1 PPTL 顺序模型
7.1.2 PPTL 并发模型
7.1.3 一个模型检测实例
7.2 离散时间区间时序逻辑统一模型检测
7.2.1、使用 TITLN建立系统模型
7.2.2、一个实例
7.2.3、TITLN统一框架模型检测
7.3 小结
第八章 基于时间区间时序逻辑的入侵检测
8.1 攻击签名逻辑与入侵检测
8.1.1 攻击签名逻辑
8.1.2 攻击模式的区间时序逻辑模型
8.1.3 实例研究
8.1.4 基于区间时序逻辑模型检测的入侵检测算法
8.1.5 prj + prj star 与 chop + chop star 的表达能力
8.2 实时攻击签名逻辑与入侵检测
8.2.1 实时攻击签名逻辑
8.2.2 基于 RASL 模型检测的入侵检测
8.2.3 实例研究
8.2.4 相关工作比较
8.3 小结
第九章 结论与展望
9.1 本文结论与创新点
9.2 下一步研究方向
致谢
参考文献
攻读博士学位期间完成的研究论文
本文编号：3739387
【文章页数】：146 页
【学位级别】：博士
【文章目录】：
摘要
ABSTRACT
第一章 绪论
1.1 研究背景与研究现状
1.1.1 模型检测
1.1.2 区间时序逻辑
1.1.3 实时系统模型检测
1.1.4 时段演算
1.1.5 基于模型检测的入侵检测
1.2 存在的问题及本文工作
1.3 论文组织结构
第二章 时序逻辑
2.1 命题投影时序逻辑
2.1.1、语法
2.1.2、语义
2.1.3、导出公式
2.2 命题区间时序逻辑
2.2.1、语法
2.2.2 语义
2.2.3 导出公式
2.3 正则图算法与满足性判定
2.3.1 正则形
2.3.2 正则图
2.4 复杂度分析
2.5 chop star 公式的满足性判定
2.5.1 扩展命题区间时序逻辑EPITL
2.5.2 EPITL 可满足性判定
2.5.3 EPITL 可满足性判定问题固有复杂度与算法复杂度
2.6 小结
第三章 实时逻辑与自动机
3.1 时间区间时序逻辑
dense-R"> 3.1.1 实界稠密时间区间时序逻辑TITL<sub>dense-R
dense-N"> 3.1.2 整界稠密时间区间时序逻辑TITL<sub>dense-N
3.1.3 实样本时间区间时序逻辑TITLsample-R
3.2 时间自动机
3.2.1、稠密时间自动机
3.2.2、离散时间自动机
3.3 时间正则表达式
3.3.1、有穷时间
3.3.2、无穷时间
3.4 离散时段演算
3.5 小结
第四章 TITL 公式可满足性判定
4.1 TITLN公式可满足性的判定问题
4.1.1 时间正则图
4.1.2 TITLN公式可满足性判定算法
4.1.3 两个例子
4.1.4 复杂度分析
4.1.5 相关工作比较
4.2 TITLR公式可满足性的判定问题
4.2.1 TITLR公式可满足性的不可判定性
4.2.2 有关TITLR公式判定性与复杂性结论
4.3 小结
第五章 TITL 模型检测
5.1 离散TITL 模型检测
5.2 稠密TITL 模型检测
5.3 相关工作比较
5.3.1 基于非时间化的TITLN判定算法的抽象描述与分析
5.3.2 两种方法比较
5.4 小结
第六章 离散TITL 表达能力
6.1 TITLN
*
6.1.2 语义
6.2 TITLN
*→TAN
*
*、TAN、TREN的等价性定理
6.6 TITLN与{┌w┐,l=k}-DCN}的等价定理
6.7 小结
第七章 统一逻辑框架模型检测
7.1 命题投影时序逻辑统一模型检测
7.1.1 PPTL 顺序模型
7.1.2 PPTL 并发模型
7.1.3 一个模型检测实例
7.2 离散时间区间时序逻辑统一模型检测
7.2.1、使用 TITLN建立系统模型
7.2.2、一个实例
7.2.3、TITLN统一框架模型检测
7.3 小结
第八章 基于时间区间时序逻辑的入侵检测
8.1 攻击签名逻辑与入侵检测
8.1.1 攻击签名逻辑
8.1.2 攻击模式的区间时序逻辑模型
8.1.3 实例研究
8.1.4 基于区间时序逻辑模型检测的入侵检测算法
8.1.5 prj + prj star 与 chop + chop star 的表达能力
8.2 实时攻击签名逻辑与入侵检测
8.2.1 实时攻击签名逻辑
8.2.2 基于 RASL 模型检测的入侵检测
8.2.3 实例研究
8.2.4 相关工作比较
8.3 小结
第九章 结论与展望
9.1 本文结论与创新点
9.2 下一步研究方向
致谢
参考文献
攻读博士学位期间完成的研究论文
本文编号：3739387
本文链接：https://www.wllwen.com/shekelunwen/ljx/3739387.html