Prop::=A[]exp|E<>exp|E[]exp|A<>exp|exp→φ
其中exp和φ为描述待验证系统性质的逻辑表达式；字符A和E用来量化路径，路径是系统的一个状态迁移序；A表示给定的性质对于所有路径均满足，E表示至少有一条路径满足给定的性质；[]和<>用来量化路径上的状态，[]表示路径上的所有状态均满足给定的性质，<>表示路径上至少有一个状态满足给定的性质。具体的逻辑语言含义如下：
A[]exp为可满足的，当且仅当对于所有路径，逻辑表达式exp在任一路径状态序列中的所有状态下均是满足的，等价于not E<>not exp；
E<>exp为可满足的，当且仅当存在一条路径，逻辑表达式exp在该路径的状态序列中的某一个状态下是满足的；
E[]exp为可满足的，当且仅当系统中存在一条路径，逻辑表达式exp在该路径状态序列中的所有状态下均是满足的；
A<>exp为可满足的，当且仅当对于所有路径，逻辑表达式exp在任一路径的状态序列中的某个状态下是满足的，等价于not E[]not exp；
Exp→φ为可满足的，当且仅当对于所有路径，逻辑表达式exp在任一路径的某一状态为真，则逻辑表达式φ必然为真，等价于A[](exp imply A<>φ)。
3      基于时间自动机的联锁进路控制流程分析
3.1    联锁软件设计开发的框架
计算机联锁系统作为一个安全苛求系统，其软件的设计和开发过程要遵循安全苛求系统的开发过程，所以我们首先给出联锁软件的设计框架，以此来开展软件设计开发的全过程。论文的研究工作也是基于这样的一个设计框架的基础上来完成的。联锁软件的设计框架是一个“V”模型，如图3.1所示：实线表示设计的流程，虚线①表示左边各个阶段的结果用于指导右边各个阶段的工作，比如应用软件的建模是根据软件的概要设计和详细设计的结果来完成的等等。虚线②表示下一阶段可能对上一阶段产生的影响和改进。
 
图3.1  联锁软件设计开发的框架模型
需求分析阶段是联锁软件开发的第一步，包括功能需求和性能需求。需求分析在整个软件生命周期是非常重要的，也是非常基础的。作好需求的分析和管理，既可以减少软件开发的许多明显错误，又可以减少修复的时间，这样从而就能够大大降低软件开发时所需要的成本，缩短软件开发的时间。
软件设计阶段是在分析联锁软件的需求基础上，利用非形式化的方法完成进路控制流程的模块化分和流程设计。
形式化建模是在流程分析的基础上利用时间自动机模型对系统进行抽象，建立描述模型。包括各个控制模块和消息处理的模型建立。在抽象的过程中，为使模型更简洁，更能反映被研究系统的实质，可以先忽略关联性小的因素。
形式化需求是根据系统的需求分析，对需求进行求精和抽象，结合系统模型用逻辑表达式进行提取。要充分考虑各种情况，抽象出来的逻辑表达式要能够全面覆盖系统的需求。模型的验证和分析就是根据需求表达式验证系统是否满足功能和性能需求，可以利用UPPAAL的模拟器和验证期对进路控制流程的各种性质进行模型检验。
3.2    联锁软件的结构
计算机联锁系统是以计算机为主要技术实现车站联锁控制的系统，计算机在系统中的作用是读入操作命令与现场的一些输入命令的表示信息，经过逻辑运算后，将结果输出给执行机构。而且，系统软件的结构还应该设置成实时操作系统的多任务系统。
综合分析国内外研制的计算机联锁系统，按照软件的层次结构，可分为三个层次[15]，即人机会话层、联锁运算层和I/O接口层，其结构如图3.2所示。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(8):http://www.751com.cn/shuxue/lunwen_767.html