| 摘要 | 第1-6页 |
| ABSTRACT | 第6-11页 |
| 第一章 绪论 | 第11-21页 |
| ·研究背景与研究现状 | 第11-18页 |
| ·模型检测 | 第11-12页 |
| ·区间时序逻辑 | 第12-14页 |
| ·实时系统模型检测 | 第14-15页 |
| ·时段演算 | 第15-17页 |
| ·基于模型检测的入侵检测 | 第17-18页 |
| ·存在的问题及本文工作 | 第18-19页 |
| ·论文组织结构 | 第19-21页 |
| 第二章 时序逻辑 | 第21-39页 |
| ·命题投影时序逻辑 | 第21-22页 |
| ·、语法 | 第21页 |
| ·、语义 | 第21-22页 |
| ·、导出公式 | 第22页 |
| ·命题区间时序逻辑 | 第22-23页 |
| ·、语法 | 第22页 |
| ·语义 | 第22页 |
| ·导出公式 | 第22-23页 |
| ·正则图算法与满足性判定 | 第23-28页 |
| ·正则形 | 第23-25页 |
| ·正则图 | 第25-28页 |
| ·复杂度分析 | 第28-30页 |
| ·chop star 公式的满足性判定 | 第30-37页 |
| ·扩展命题区间时序逻辑EPITL | 第30页 |
| ·EPITL 可满足性判定 | 第30-35页 |
| ·EPITL 可满足性判定问题固有复杂度与算法复杂度 | 第35-37页 |
| ·小结 | 第37-39页 |
| 第三章 实时逻辑与自动机 | 第39-51页 |
| ·时间区间时序逻辑 | 第39-43页 |
| ·实界稠密时间区间时序逻辑TITL__(dense-R) | 第39-40页 |
| ·整界稠密时间区间时序逻辑TITL__(dense-N) | 第40-41页 |
| ·实样本时间区间时序逻辑TITL_(sample-R) | 第41页 |
| ·整样本时间区间时序逻辑TITL_(sample-N) | 第41-42页 |
| ·TITL__(dense-R) 、TITL__(dense-N) 、TITL_(sample-R) 和TITL_(sample-N) 的关系 | 第42-43页 |
| ·时间自动机 | 第43-47页 |
| ·、稠密时间自动机 | 第43-46页 |
| ·、离散时间自动机 | 第46-47页 |
| ·时间正则表达式 | 第47-48页 |
| ·、有穷时间 | 第47页 |
| ·、无穷时间 | 第47-48页 |
| ·离散时段演算 | 第48-49页 |
| ·小结 | 第49-51页 |
| 第四章 TITL 公式可满足性判定 | 第51-81页 |
| ·TITL_N公式可满足性的判定问题 | 第51-78页 |
| ·时间正则图 | 第51-63页 |
| ·TITL_N公式可满足性判定算法 | 第63-72页 |
| ·两个例子 | 第72-74页 |
| ·复杂度分析 | 第74-78页 |
| ·相关工作比较 | 第78页 |
| ·TITL_R公式可满足性的判定问题 | 第78-80页 |
| ·TITL_R公式可满足性的不可判定性 | 第78-80页 |
| ·有关TITL_R公式判定性与复杂性结论 | 第80页 |
| ·小结 | 第80-81页 |
| 第五章 TITL 模型检测 | 第81-97页 |
| ·离散TITL 模型检测 | 第81-91页 |
| ·稠密TITL 模型检测 | 第91页 |
| ·相关工作比较 | 第91-96页 |
| ·基于非时间化的TITL_N判定算法的抽象描述与分析 | 第92-95页 |
| ·两种方法比较 | 第95-96页 |
| ·小结 | 第96-97页 |
| 第六章 离散TITL 表达能力 | 第97-107页 |
| ·TITL_N~* | 第97-99页 |
| ·语法 | 第97-98页 |
| ·语义 | 第98-99页 |
| ·TITL_N~*→TA_N | 第99-102页 |
| ·TA_N→TRE_N | 第102-103页 |
| ·TRE_N→TITL_N~* | 第103-105页 |
| ·TITL_N~*、TA_N、TRE_N的等价性定理 | 第105页 |
| ·TITL_N与{┌w┐,l=k}-DC_N}的等价定理 | 第105-106页 |
| ·小结 | 第106-107页 |
| 第七章 统一逻辑框架模型检测 | 第107-117页 |
| ·命题投影时序逻辑统一模型检测 | 第107-110页 |
| ·PPTL 顺序模型 | 第107-108页 |
| ·PPTL 并发模型 | 第108-109页 |
| ·一个模型检测实例 | 第109-110页 |
| ·离散时间区间时序逻辑统一模型检测 | 第110-115页 |
| ·、使用 TITLN建立系统模型 | 第110-113页 |
| ·、一个实例 | 第113-115页 |
| ·、TITLN统一框架模型检测 | 第115页 |
| ·小结 | 第115-117页 |
| 第八章 基于时间区间时序逻辑的入侵检测 | 第117-129页 |
| ·攻击签名逻辑与入侵检测 | 第117-125页 |
| ·攻击签名逻辑 | 第117-118页 |
| ·攻击模式的区间时序逻辑模型 | 第118-119页 |
| ·实例研究 | 第119-122页 |
| ·基于区间时序逻辑模型检测的入侵检测算法 | 第122-123页 |
| ·prj + prj star 与 chop + chop star 的表达能力 | 第123-125页 |
| ·实时攻击签名逻辑与入侵检测 | 第125-127页 |
| ·实时攻击签名逻辑 | 第125页 |
| ·基于 RASL 模型检测的入侵检测 | 第125-126页 |
| ·实例研究 | 第126-127页 |
| ·相关工作比较 | 第127页 |
| ·小结 | 第127-129页 |
| 第九章 结论与展望 | 第129-131页 |
| ·本文结论与创新点 | 第129-130页 |
| ·下一步研究方向 | 第130-131页 |
| 致谢 | 第131-133页 |
| 参考文献 | 第133-145页 |
| 攻读博士学位期间完成的研究论文 | 第145-146页 |
