模型检测是一种基于形式化方法的自动分析和验证技术,问题的关键是状态空间爆炸的解决。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检测,得到一些安全协议的相关分析结果,为网络安全协议提供了可行的分析与检测方法。