2.3.1    UPPAAL的结构和特征
本课题采用UPPAAL来进行建模，UPPAAL采用图形化的界面，可以适用于Windows、Linux、SunOS、MACOS等多种系统。其体系结构如图2.1所示。
 
图2.1  UPPAAL的体系结构
UPPAAL工具主要由系统编辑器、模拟器和验证器组成。系统编辑器主要用来创建和编辑需要分析的实时系统，他们被描述为一系列过程模板，一些全局声明，过程分配和一个系统定义。模拟器是一个确认工具，它在系统早期的设计阶段就可以对所有可能的执行序列进行检查，这样可以提前就发现一些明显错误。验证器通过快速搜索系统的状态空间来检查简单不变式、系统的安全性、可达性以及受限性等。另外，过程模板带有参数，给模板传递不同的参数可得到不同的过程，因此通过设计模板可以描述控制结构相同的多个过程。同时它还为系统要求的规范提供了一个需求规范编辑器。
UPPAAL中使用的是时间自动机模型，并对时间自动机进行了一些扩展。可以声明一般值变量，全局时钟和用于同步的通道。它在位置和通道上都对时间自动机进行了改进：
（1）  位置
时间自动机中的位置节点表示时间过程的控制位置，英文为Location，每一个位置都伴随有时钟约束。UPPAAL中对时间自动机的位置有所改进，除了已有的起始位置和普通位置外，又增加了紧迫位置和约束位置，英文名分别为urgent location和committed location，在紧迫位置没有时间延迟，使用它可以减少模型中时钟的个数，减少模型的复杂度。如果一个位置是紧迫位置，在时间自动机网络中用U来标记。当系统处于约束位置时，时间过程的执行不能被打断，而执行过程也不消耗时间。约束位置在时间自动机网络中用C标记。约束位置的使用可以显著减少状态空间，但是要慎重使用它，因为它可能会导致死锁。
（2）  通道
通道英文为Channal，主要用于保证多个进程模板的同步通信和相互操作。这可以通过在不同进程模板的转移边上标注互补的同步标记得以实现。例如，给定一个通道n，那么n！和n？就是互补的同步标记，分别表示在通道n上发送和接收同步信号。通道可以被声明为紧迫通道和广播通道，英文为urgent channel和broadcast channel。UPPAAL中增加了紧迫通道，它与普通通道的区别在于转换时它没有时间上的延迟。广播通道允许一对多的同步操作。如果带有同步标志n！的转移边在通道上发出一条广播消息，那么任何带有同步标记n？的使能转移边将和发送进程保持同步。
2.3.2    UPPAAL的系统描述语言
UPPAAL中所使用的系统描述语言是一种类似于C/C++/Java的语言。它用于描述事件自动机网络，其中，扩展有CSS样式同步、广播同步、过程模板、有限整数、常量、数组等对象。下面重点介绍UPPAAL中存在的集中约束形式和规范验证语言BNF。
（1）  数值约束
UPPAAL中用户可以定义一般值变量和全局变量等，变量的使用就会产生数值约束，较之Alur时间自动机，UPPAAL中存在三种形式的约束，即：
g::=g_clock|g_data|g,g
其中：
g_clock::=x<n|x<=n|x==n|x>=n|x>n
g_data::=ex<ex|ex<ex|ex==ex|ex!=ex|ex>=ex|ex>ex
Ex::=n|v(ex)|-ex|ex+ex|ex-ex|ex*ex|ex/ex|(g_data?ex,ex)
（2）  验证语法
使用UPPAAL对实时系统进行验证时，首先用时序逻辑公式给出待验证的形式化需求规范，然后在时间自动机网络系统状态空间模型中搜索满足的状态，判断系统是否满足待验证的性质。UPPAAL使用的时序逻辑公式是时间分支时序逻辑的子集，称为UPPAAL需求规范语言，其BNF语法如下： 车站联锁系统UPPAAL建模+时间自动机模型进行模拟仿真(7):http://www.youerw.com/shuxue/lunwen_767.html