基于UPPAAL的复杂定时数据建模

，,2，

(1.郑州大学 信息工程学院， 郑州 450001; 2.吉首大学 数学与计算机科学学院，湖南 吉首 416000)

模型检测技术是一种形式化验证技术，不同的建模方法具有不同的特点。进程代数方法在验证协议的交互行为方面具有优势，但不利于对协议的时间行为进行验证。基于时间自动机的建模方法是对协议的时间行为进行建模的主流方法，UPPAAL是其代表性建模工具，是高效的实时系统验证工具。其典型的应用例子有TDMA协议的启动机制验证[1]、Bang & Olufsen公司的音视频系统故障[2]、变速箱的自动验证[3]等。

用UPPAAL对带有一定生存时间的多个同类数据进行描述时，现有的建模方法并不能很好地应用。一般地，UPPAAL表示有一定生存时间的一条数据或其行为时，采用时间自动机在模型内部直接描述的方法，以便将数据的行为完全内嵌到系统模型中。其优势是简单和高效，但对于具有不同生存时间的多条数据进行建模时，这种方法却不再适用。这一方面在于此方法须为每条数据提供若干控制位置，会显著增大模型规模；另一方面因为此方法的灵活性差，不能适应数据的随机存储和处理，使整个系统的可扩展性变差。在路由协议的特殊情况下，甚至难以用现有方法进行建模。本文的关键在于提出一种基于时间分片的解决方法。

1 相关知识

时间自动机是自动机的扩展，在传统自动机的迁移系统中加入了延时迁移功能，用于描述时间的流逝[4]。UPPAAL工具进一步增强了时间自动机的功能，在建模时加入变量和类似于C语言语法的自定义函数，以便更容易地描述待验证系统[5]。很多带有数组变量的模型都采用专门的自动机来管理数据结构，使得模型能以简单的方式管理复杂的数据[6]。虽然加入了变量并且支持数组和结构体类型，但UPPAAL工具提供的变量管理机制并不支持定时数据。而对于网络协议来说，时效性是必须考虑的问题，因此本文提出了一种为多条数据时效性建模的方法。

时间自动机的定义(定义1)：一个时间自动机是一个五元组<Σ,S,S0,C,E>，其中Σ是有限的字母表，S是状态的一个有限集，S0⊆S是开始状态的集合，C是时钟的有限集合，E⊆S×S×Σ×2C×Φ(C)是迁移的集合。边表示输入字符是a时，从状态s到状态s′的迁移。

UPPAAL中扩展了时间自动机的表达能力，其定义(定义2)如下：UPPAAL中的时间自动机是一个七元组，其中S是有限集合，s0∈S表示初始状态，A是动作的集合，C是时钟的有限集合，V是数据变量的集合，I∶S→Φ(C,V)将一个状态映射为一个不变式(invariant)，E⊆S×Φ(C,V)×A×R(C,V)×S是边的集合。

2 问题描述

2.1 定时数据及其应用

在OLSR等ad hoc路由协议中，路由器要存储关于链路和拓扑的各种信息。这些信息分别以链路集合和拓扑集合的形式存储。这些集合有特定的生存周期，超过生存周期后，集合里的信息就视为无效，数据应被删除。这类数据称为定时数据。同步定时数据是指一组有效期相同的，同时更新、同时过期的定时数据。

定义3 定时数据(TimedData，TD)是一个两元组，其中TD是数据的集合，T是数据的生存周期，对于c∈C，TD满足以下关系：

if:T(i)

定义4 同步定时数据(SynchronizedTimedData，STD)是一个两元组。其中，STD⊆V是数据的集合；t是STD中数据的生存周期。对于c∈C，STD满足以下关系：

其中STD(0)=∪stdi(0),if:stdi∈STD

在OLSR路由协议中，各节点都维护着各自的链路集。链路集内的各条数据表示节点与其邻居之间的可用链路，每条数据有自身的生存时间。节点通过周期性地发送HELLO消息来维护链路集。若在生存时间到期前收到了来自某邻居的HELLO消息，则更新相对应的元组；否则，链路集内的数据条目会在到期后被删除[7]。当前版本的UPPAAL(UPPAAL 4.1.18)不具有触发器的功能，即不支持为单个数据设置时钟并在数据到期后将之删除。为描述这类带有时间特性的数据行为，需要用专门的自动机为其建模。

网络中有若干路由器，上面运行着OLSR路由协议。每个路由器维护着各自的链路信息、邻居信息、拓扑信息和路由信息等。为简化模型，这里只考虑链路信息。LinkSet是链路信息的集合，路由器通过LinkSet维护链路信息。每条链路信息就是一个五元组linkTuple:=。其中：L_local_iface_addr表示路由器的本地接口地址；L_neigh_iface_addr表示与此路由器通信的邻居路由器的接口地址；L_SYM_time表示链路状态是双向的生存时间；L_ASYM_time表示链路状态是单向的生存时间；L_time表示元组的生存时间。当L_time的生存期满之后，整个元组将被删掉，表示这条链路已不再可用。L_SYM_time在生存期内意味着L_local_iface_addr和L_neigh_iface_addr之间的连接是双向的，即任意一方均可收到对方发来的消息，而其生存期满意味着L_local_iface_addr和L_neigh_iface_addr之间的连接不再是双向的，即可能是单向的或者已经断开。L_ASYM_time在生存期内意味着L_local_iface_addr可以接收到来自L_neigh_iface_addr的数据，而其生存期满意味着L_local_iface_addr和L_neigh_iface_addr之间已经断开连接。

一个元组就是一条定时数据。路由器维护的链路集中的多个元组构成一组难以建模的复杂定时数据。

2.2 原有建模模板的局限

2.2.1 同步定时数据建模模板

系统更新过的数据在一定生存时间后会失效。系统会在数据失效时，将这组数据删除。这类系统的例子有电梯系统、ATM机系统和一个分析转盘系统[8]等。其特点是数据可在任意时刻到达，但只在一段时间内有效，下次被激活的时间并不固定(见图1)。

图1 一组同步定时数据的建模方法

这种方法可以方便地管理系统中的同步定时数据。但对于OLSR协议的建模与验证问题来说，这种建模模板太简单，无法全面描述各节点的中间信息。

2.2.2 周期性更新的定时数据建模模板

多条数据的有效期相同并且只在特定的时钟周期上改变值或有效性，如实时监测温度和湿度信息的轮询系统等。其特点是数据周期性地发生变化。上面提到的建模方法就显得非常复杂，在变量个数不确定的情况下(比如网络和系统交互时的中间信息)，甚至会无法建模。这类系统如图2所示。

图2 相同有效期变量的建模

这种建模方法即使做了扩展，仍然不能对OLSR协议中的数据结构建模，因为OLSR协议的数据可以在任意时刻发生变化，并不会局限在固定的时钟周期上。

3 复杂定时数据建模的方法

对带有复杂定时数据的系统来说，通常对时间的建模是内嵌在模型里的，若各条数据结构都含有生存时间，即数据有效性会在定时器到期时发生变化，则通常的建模方法会变得相当复杂；若多条数据结构中都含有独立的生存时间，则普通的方法完全无法正确建模。

在路由协议中，多个节点可能在任意时刻发起通信，并在接收到消息包后更新各自的局部变量。其中复杂定时数据的特点是多条数据的有效期是固定的时间段，但对这些数据进行的更新可能发生在任意时刻。因为UPPAAL工具没有提供类似定时器变量的机制，故难以精确地刻画变量的生存时间，但可以采用非精确的时间分片策略来取得结果。这种方法借鉴了早期计算机操作系统中的忙等方法，即每隔一段时间检查一下变量，并更新数据的生存时间。这种情形下的建模模板如图3所示。图3(a)中的自动机是更新自动机，负责每过一个时间片对数据的有效性进行一次检查。这个检查过程独立于发送周期和各自的生存周期。在checkTime()函数所在的边上加入条件x

图3 复杂定时变量的建模

在图3所示的模型中，由于对数据生存时间的更新只能发生在INTERVAL的倍数时间上，故而所提出的方法能表示的精度有限，即精度为INTERVAL。这种表示方法虽然有精度上的缺陷，但却不影响对OLSR路由协议的验证，其原因在于，OLSR协议中的每个节点对链路信息都有一个保持时间(HOLD TIME)，当发现链路断开后，还要经过一个保持时间，链路才会真正断开。保持时间通常和HELLO的发送周期相同，并且模型中又忽略了链路丢包的情形，故只需INTERVAL的值相对于保持时间来说较小，即可保证时间片的精度不会影响所需验证的原系统的重要性质。因此，这种方法的误差不至于导致协议主要性质的改变。

在复杂定时变量建模方法中，每隔一小段时间必须检查一次变量，使得系统增加大量的额外操作。若设置的时间间隔过小，则验证耗时会成倍增长，时间代价会非常巨大。为了兼顾精确度和时间代价，通常选择INTERVAL为HOLD_TIME的五分之一到三分之一。

4 建模方法的应用

本文以OLSR协议中HELLO消息的传输和存储为应用背景，以链路信息为例，验证协议的链路保持功能和对链路断开的敏感性。选择的系统是一个运行OLSR协议的网络，有6个运行OLSR协议的节点。一个节点的行为用一个自动机描述，用一个自动机判断网络是否收敛，并在网络收敛后控制一条链路断开，再让此自动机处于另一个位置，最后根据此位置验证节点对链路断开的敏感性。使用本文提出的方法为各节点的链路信息建模，建模结果如图4所示。6个自动机分别模拟了各个节点。

图4 OLSR协议中的链路信息示例模型

为了验证图4所示模型对链路中断的敏感性,本文采用如下两条性质：

(1)(Controller.L1 and Controller.x< HOLD_TIME-INTERVAL)

imply (Node(node_A).neigh [node_B]==1 and Node(node_B).neigh[node_A]==1)

这条性质指在网络收敛后，若1和3之间的链路断开，则在本地信息中的链路将继续保留HOLD_TIME-INTERVAL个时间单位。

(2) (Controller.L1 and Controller.x< HOLD_TIME-INTERVAL)

imply (Node(node_A).neigh [node_B]==0 and Node(node_B).neigh[node_A]==0)

这条性质是指在网络收敛后，若node_A和node_B之间的链路断开，且时间超过HOLD_TIME个时间单位，则在本地链路信息中显示node_A和node_B之间的链路已被删除。

验证所采用的平台为联想ThinkStation D20，12G内存，3.07GHz *19英特尔Xeon CPU，64位Ubuntu12.04 操作系统。验证结果如图5所示，表明模型较好地描述了原系统。

图5 示例模型的验证结果

5 结 语

本文解决了采用模型检测技术验证路由协议的建模难题。对路由协议中的复杂定时数据建模，本质上是为数据有效性随时间变化的行为进行建模。本文提出的方法首先对数据的生存时间进行离散化处理，然后通过得到的时间分片对生存时限进行建模，最后由管理自动机进行统一管理，从而解决复杂定时数据的建模难题。对OLSR协议的链路保持功能进行验证的结果表明，本文提出的方法可以有效地对复杂定时数据建模。本文提出的方法可在网络协议的验证过程中满足要求，但对于时间精度要求更高的实时系统，其精度问题仍会影响系统的重要性质。另外，大量的空转操作严重影响验证的性能。

下一步的研究是进一步细化此建模方法，以便在精度和时间代价上取得更好的平衡。并且，针对时间间隔过短造成的验证时间急剧增加问题，重点研究精确加速技术，以便在高验证精度之下加快验证速度。

参考文献:

[1] Lonn H, Pettersson P.Formal Verification of a TDMA Protocol Startup Mechanism [C]//Bob Werner.Pacific Rim International Symposium on Fault-Tolerant SystemsLos Alamitos.California: IEEE computer Society, 1997: 235-242.

[2] Havelund K, Skou A, Larsen K G.Formal Modelling and Analysis of an Audio/Video Protocol: An Industrial Case Study Using UPPAAL[C]//Bob Werner.The 18th IEEE Real-Time Systems Symposium Los Alamitos.California: IEEE Computer Society, 1997: 2-13.

[3] Lindahl M, Pettersson P, Wang Yi.Formal Design and Analysis of a Gearbox Controller[J].International Journal on Software Tools for Technology Transfer, 2001, 3(3): 353-368.

[4] Alur R, Dill D.A Theory of Timed Automata[J].Theoretical Computer Science, 1994, 126(2): 183-235.

[5] Behrmann G, David A, Larsen K G.A tutorial on uppaal[C]//Formal methods for the design of real-time systems.Berlin: Springer Berlin Heidelberg, 2004: 200-236.

[6] Ravn A P, Srba J, Vighio S.A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL[C]//Tiziana Margaria.Leveraging Applications of Formal Methods, Verification, and Validation.Berlin: Springer Berlin Heidelberg, 2010: 579-593.

[7] Clausen T, Jacquet P.Optimized Link State Routing Protocol (OLSR) [EB/OL].[2014-03-12].http://www.ietf.org/rfc/rfc3626.txt.

[8] Davor S, John H, Jagadish S, et al.Analyzing a Pattern-Based Model of a Real-Time Turntable System[J].Electronic Notes in Theoretical Computer Science, 2009, 25(1): 161-178.