形式化规范可以精确地描述系统模型，排除了矛盾、二义性、含糊性等情况；同时，在对系统进行严格的描述的过程中，将会帮助用户明确其原本模糊的需求，并发现用户所陈述的需求中存在的矛盾等情况，从而相对完整、正确地理解用户需求，最终得到一个完整、正确的系统模型。
2.1.2    形式化验证
形式化验证方法是指使用严格的数学方法来推理验证产品或设计是否符合其全部或部分规范的过程。在形式化方法中，在开发出形式化规范后就进行形式验证，既可以提前发现错误，同时在修改发现的错误时需要付出的代价也是最小的。目前形式验证主要有两种方法：模型检验和定理证明。
模型检验是一种基于有限状态模型并检验该模型的期望特性的技术。模型检验主要适用于有穷状态系统，其优点是完全自动化并且验证速度快；模型检验离不开模型检验工具的支持，很多研究机构和大学开发了实际的模型检验工具，比如美国Carnegie Mellon大学的SMV，BELL实验室的SPIN，以及丹麦的Aalborg大学和瑞典的UPPASLS大学联合开发的UPPAAL等等。
定理证明采用逻辑公式来规范系统及其性质，其中的逻辑出一个具有公理和推理规则的形式化系统给出，进行定理证明的过程就是应用这些公理或推理规则来证明系统具有某些性质。不同于模型检验，定理证明可以处理无限状态空间问题，它使用类似于结构化的推导过程来证明具有无限状态的系统。
2.2    时间自动机理论
自动机理论主要研究离散数字系统的功能、结构及其关系。随着微电子技术和信息科学的发展，自动机理论向信息技术的各个应用领域发展，为它们提供理论模型、设计技术和运行算法。自动机理论的研究领域主要包括：有限自动机理论、无限自动机理论、概率自动机理论、复自动机理论以及抽象自动机理论等。
由于自动机可以描述现实世界中各种离散数字系统的共同特征，因此自动机的研究在经济、神经、生物、通讯、智能和检测等各个领域都得到了广泛的应用。同时，由于自动机自然地包含状态和事件等描述离散事件动态系统的基本要素，所以理所当然地成为DEDS中的被控对象、监控器和整个闭环系统的重要逻辑层模型之一。它作为计算机科学基础理论的研究，直接地推动计算机科学技术的发展。当前，在这一方面的研究十分活跃，在理论上有了很大的进展，其研究与计算机的软、硬件的发展直接相关。
时间自动机是为解决实时系统建模和验证而对自动机理论的扩展，它是为了适应实时系统的验证需要，由R.Alur等人提出的理论。时间自动机提供了一种简单有效的方法来描述带有时间因素的系统状态转换图，因此是一种实时系统的行为建模以及自动验证工具的开发提供了重要的理论基础。在实时系统的规范说明和模型验证中占据重要地位。本文使用的UPPAAL工具就是以时间自动机理论为基础的。
2.3    模型分析验证工具UPPAAL介绍
UPPAAL是由丹麦的Aalborg大学和瑞典的UPPSALA大学于1995年联合开发的自动验证工具，是具有世界先进水平的实时系统模拟和验证工具。UPPAAL主要采用一组带有整型变量的时间自动机对实时系统的行为进行模拟，对它的性质进行验证。UPPAAL采用的模型验证机制可以避免状态空间爆炸问题，它已经被广泛应用于算法分析和协议验证方面。一个实时系统模型包含一组带有有限控制结构和实数时终值的非确定性进程，这些控制结构和时钟变量可以通过通道以及共享全局变量进行相互通信。UPPAAL的主要优点是其运作的高效性和使用的方便性。 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(6):http://www.youerw.com/shuxue/lunwen_767.html