基于行为时序逻辑模型检测的研究与应用

摘要

模型检测是一种基于形式化方法的自动分析和验证技术，问题的关键是状态空间爆炸的解决。Lesilie Lamport提出行为时序逻辑（TLA）理论体系，运用TLA对软件或协议进行建模，它能在一种语言中同时表达程序与属性，在理论和实际应用中，这种模型检测技术具有一定研究价值。
　　本文在详细介绍行为时序逻辑基本概念的基础上，分析了使用行为时序逻辑基本理论对并发系统的建模，运用TLA+规约语言与检测工具对并发系统和网络安全协议进行简要分析与检测，所作的主要工作与创新之处如下：
　　1、在行为时序逻辑（Temporal Logic of Action）的基础上严格定义了行为
　　路径对行动的强弱公平性，并详细证明了并发系统中行为对行动的强弱公平性，介绍 TLA语法与语义，并分析TLA的逻辑推理规则，以简单程序实例分析和证明并发系统所具有的不变性，对程序的不同 TLA时序公式之间等价性进行分析；
　　2、TLA+是基于TLA的描述并发系统的规约语言，阐述了使用TLA+语言描述并发系统的规约方法，分析检测工具 TLC的结构组成、各命令参数的功能及检测原理及要求，研究了协议的分析、建模及检测流程；
　　3、基于TLA的网络协议与并发系统模型的形式化建模、分析与检测，以时钟并发系统为实例进行TLA+建模与分析，并给出系统所需满足的一些基本性质的TLA时序公式，通过 TLC工具检测，系统满足这些属性；
　　4、提出使用基于TLA对网络安全协议分析与检测的分析与研究，对 NS协议进行形式化分析，建立了入侵者参加的简化模型，通过对模型进行FSM建模，严格转化为TLA+描述的规约系统，然后对其进行TLC检测，得到一些安全协议的相关分析结果，为网络安全协议提供了可行的分析与检测方法。

目录

封面

目录

中文摘要

英文摘要

第一章 引 言

§1．1 并发系统

§1．2 形式化验证方法

§1．3 Kripke 结构与标记转移系统

§1．4 模型检测

§1．5 逻辑和程序

§1．6 论文的结构安排

第二章 行为时序逻辑

§2．1 基本概念

§2．2 简单时序逻辑

§2．3 基本时序逻辑

§2．4 TLA

第三章 程序的相关属性分析

§3．1 不变性

§3．2 并发系统事件的可能性

§3．3 程序不同 TLA 公式的等价性分析

第四章 描述语言 TLA+及检测工具 TLC

§4．1 TLA+的模块结构

§4．2 TLA+操作符

§4．3 检测工具 TLC 及使用

§4．4 完整的时钟规约系统

§4．5 并发转移系统的规约系统性质的检测与验证

第五章 基于 TLA 的协议描述与检测

§5．1 有限状态机

§5．2 基于 TLA 的并发系统的建模

§5．3 NSPK 协议的 TLA 的描述与检测

总结与展望

致谢

参考文献

附 录

声明