车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(5)
（2） 计算机联锁的优点
与继电集中联锁相比，计算机联锁具有以下显著优点：
进一步提高了安全性、可靠性，增加和完善了功能，方便设计，省工省料，降低造价。最重要的是，计算机联锁系统为铁路信号向智能化和网络化方向发展创造了条件。
1.3 选题的目的和意义
铁路信号系统是为保证铁路运输安全设的，铁路车站信号联锁系统是铁路信号系统的重要组成部分，车站联锁软件是一种典型的安全性软件。车站联锁软件也是一种实时系统，实时系统不仅要求所得出的结果在逻辑上是正确的，而且在时间上也要是正确的，为了保证车站联锁系统的正确性和安全性，采用形式化方法对其进行描述、和分析是非常重要的。铁路车站信号联锁系统逻辑的形式化描述就计算机联锁软件的开发和联锁软件的测试，都是非常重要的。铁路车站的联锁逻辑相当复杂，对其进行形式化描述是一项艰难的任务，为了对实时系统行为进行建模，引入了时间自动机对实时系统行为进行建模的方法。UPPAAL这个软件是一种基于时间自动机的实时系统的模型检测软件，它可以对实时系统建模、确认和验证，是一种发展成熟，功能强大的模型验证工具。
通过比较发现，时间自动机比较适合进行联锁的形式化建模和分析。因为时间自动机是一种描述实时系统的形式化方法，在实时系统中和模型验证中占重要地位[12]。更主要的是以时间自动机为模型的UPPAAL软件功能强大、发展成熟，并且它的通用性非常好，可以有效进行建模、模拟。利用时间自动机模型UPPAAL对计算机联锁软件进行建模和验证，可以大大减小由开发人员造成的设计故障，提高系统的安全性。这对于联锁软件的开发和测试都有十分重要的意义，同时也为基于通信的列车运行控制系统的研发和测试提供了帮助。
2 时间自动机理论和UPPAAL介绍
2.1 形式化方法概述
随着计算机技术在信号系统中的广泛应用，计算机技术带来了效率，同时也带来了一些安全隐患。信号系统的越来越复杂，急需一种方法来对系统的性能和功能进行分析和验证。目前，研究者偏向于使用形式化方法来开展工作。
形式化方法使用严格的数学符号和数学法则对目标软件系统的结构与行为进行有效的综合、分析和推理，为系统的说明、开发和验证提供了一个框架，有利于发现目标软件系统需求中的不一致性、不完整性等。从广义的角度，形式化方法是软件开发过程中分析、设计及实现的系统工程方法。而从狭义的角度，形式化方法又是软件规范和验证的方法。因此，形式化方法又分为形式化规范方法和形式化验证方法。
2.1.1 形式化规范
形式化方法的一个重要研究内容是形式化规范，它是用具有精确语义的形式语言书写的程序功能描述，是设计和编制程序的出发点，也是验证程序是否正确的依据。
从形式化规范到目标软件系统的可实现和可执行角度，已建立的形式化方法可分为三类：操作类、描述类和双重类[12-14]。操作类方法基于状态和转移，通过可执行模型来描述系统，模型本身能够采用静态分析和模型执行得到验证，比如有限状态机，时间自动机，Petri网等；描述类方法基于数学公式和概念，通过逻辑或代数给出系统的状态空间，具有高度抽象的特点，如Z、VDM、Larch、CTTL等；双重类方法则兼有前面二者的特点，既能够通过数学公理和概念来高度抽象地描述系统，又具有状态和转移的可执行特征，如扩展状态机/实时事态逻辑、TRIO+、TROL等。
下一篇：投资者情绪与股票收益率的关系研究