，,2，

(1.鄭州大學(xué) 信息工程學(xué)院， 鄭州 450001; 2.吉首大學(xué) 數(shù)學(xué)與計(jì)算機(jī)科學(xué)學(xué)院，湖南 吉首 416000)

模型檢測技術(shù)是一種形式化驗(yàn)證技術(shù)，不同的建模方法具有不同的特點(diǎn)。進(jìn)程代數(shù)方法在驗(yàn)證協(xié)議的交互行為方面具有優(yōu)勢，但不利于對協(xié)議的時(shí)間行為進(jìn)行驗(yàn)證?；跁r(shí)間自動(dòng)機(jī)的建模方法是對協(xié)議的時(shí)間行為進(jìn)行建模的主流方法，UPPAAL是其代表性建模工具，是高效的實(shí)時(shí)系統(tǒng)驗(yàn)證工具。其典型的應(yīng)用例子有TDMA協(xié)議的啟動(dòng)機(jī)制驗(yàn)證[1]、Bang & Olufsen公司的音視頻系統(tǒng)故障[2]、變速箱的自動(dòng)驗(yàn)證[3]等。

用UPPAAL對帶有一定生存時(shí)間的多個(gè)同類數(shù)據(jù)進(jìn)行描述時(shí)，現(xiàn)有的建模方法并不能很好地應(yīng)用。一般地，UPPAAL表示有一定生存時(shí)間的一條數(shù)據(jù)或其行為時(shí)，采用時(shí)間自動(dòng)機(jī)在模型內(nèi)部直接描述的方法，以便將數(shù)據(jù)的行為完全內(nèi)嵌到系統(tǒng)模型中。其優(yōu)勢是簡單和高效，但對于具有不同生存時(shí)間的多條數(shù)據(jù)進(jìn)行建模時(shí)，這種方法卻不再適用。這一方面在于此方法須為每條數(shù)據(jù)提供若干控制位置，會顯著增大模型規(guī)模；另一方面因?yàn)榇朔椒ǖ撵`活性差，不能適應(yīng)數(shù)據(jù)的隨機(jī)存儲和處理，使整個(gè)系統(tǒng)的可擴(kuò)展性變差。在路由協(xié)議的特殊情況下，甚至難以用現(xiàn)有方法進(jìn)行建模。本文的關(guān)鍵在于提出一種基于時(shí)間分片的解決方法。

1 相關(guān)知識

時(shí)間自動(dòng)機(jī)是自動(dòng)機(jī)的擴(kuò)展，在傳統(tǒng)自動(dòng)機(jī)的遷移系統(tǒng)中加入了延時(shí)遷移功能，用于描述時(shí)間的流逝[4]。UPPAAL工具進(jìn)一步增強(qiáng)了時(shí)間自動(dòng)機(jī)的功能，在建模時(shí)加入變量和類似于C語言語法的自定義函數(shù)，以便更容易地描述待驗(yàn)證系統(tǒng)[5]。很多帶有數(shù)組變量的模型都采用專門的自動(dòng)機(jī)來管理數(shù)據(jù)結(jié)構(gòu)，使得模型能以簡單的方式管理復(fù)雜的數(shù)據(jù)[6]。雖然加入了變量并且支持?jǐn)?shù)組和結(jié)構(gòu)體類型，但UPPAAL工具提供的變量管理機(jī)制并不支持定時(shí)數(shù)據(jù)。而對于網(wǎng)絡(luò)協(xié)議來說，時(shí)效性是必須考慮的問題，因此本文提出了一種為多條數(shù)據(jù)時(shí)效性建模的方法。

時(shí)間自動(dòng)機(jī)的定義(定義1)：一個(gè)時(shí)間自動(dòng)機(jī)是一個(gè)五元組<Σ,S,S0,C,E>，其中Σ是有限的字母表，S是狀態(tài)的一個(gè)有限集，S0?S是開始狀態(tài)的集合，C是時(shí)鐘的有限集合，E?S×S×Σ×2C×Φ(C)是遷移的集合。邊表示輸入字符是a時(shí)，從狀態(tài)s到狀態(tài)s′的遷移。

UPPAAL中擴(kuò)展了時(shí)間自動(dòng)機(jī)的表達(dá)能力，其定義(定義2)如下：UPPAAL中的時(shí)間自動(dòng)機(jī)是一個(gè)七元組，其中S是有限集合，s0∈S表示初始狀態(tài)，A是動(dòng)作的集合，C是時(shí)鐘的有限集合，V是數(shù)據(jù)變量的集合，I∶S→Φ(C,V)將一個(gè)狀態(tài)映射為一個(gè)不變式(invariant)，E?S×Φ(C,V)×A×R(C,V)×S是邊的集合。

2 問題描述

2.1 定時(shí)數(shù)據(jù)及其應(yīng)用

在OLSR等ad hoc路由協(xié)議中，路由器要存儲關(guān)于鏈路和拓?fù)涞母鞣N信息。這些信息分別以鏈路集合和拓?fù)浼系男问酱鎯?。這些集合有特定的生存周期，超過生存周期后，集合里的信息就視為無效，數(shù)據(jù)應(yīng)被刪除。這類數(shù)據(jù)稱為定時(shí)數(shù)據(jù)。同步定時(shí)數(shù)據(jù)是指一組有效期相同的，同時(shí)更新、同時(shí)過期的定時(shí)數(shù)據(jù)。

定義3 定時(shí)數(shù)據(jù)(TimedData，TD)是一個(gè)兩元組，其中TD是數(shù)據(jù)的集合，T是數(shù)據(jù)的生存周期，對于c∈C，TD滿足以下關(guān)系：

if:T(i)

定義4 同步定時(shí)數(shù)據(jù)(SynchronizedTimedData，STD)是一個(gè)兩元組。其中，STD?V是數(shù)據(jù)的集合；t是STD中數(shù)據(jù)的生存周期。對于c∈C，STD滿足以下關(guān)系：

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

在OLSR路由協(xié)議中，各節(jié)點(diǎn)都維護(hù)著各自的鏈路集。鏈路集內(nèi)的各條數(shù)據(jù)表示節(jié)點(diǎn)與其鄰居之間的可用鏈路，每條數(shù)據(jù)有自身的生存時(shí)間。節(jié)點(diǎn)通過周期性地發(fā)送HELLO消息來維護(hù)鏈路集。若在生存時(shí)間到期前收到了來自某鄰居的HELLO消息，則更新相對應(yīng)的元組；否則，鏈路集內(nèi)的數(shù)據(jù)條目會在到期后被刪除[7]。當(dāng)前版本的UPPAAL(UPPAAL 4.1.18)不具有觸發(fā)器的功能，即不支持為單個(gè)數(shù)據(jù)設(shè)置時(shí)鐘并在數(shù)據(jù)到期后將之刪除。為描述這類帶有時(shí)間特性的數(shù)據(jù)行為，需要用專門的自動(dòng)機(jī)為其建模。

網(wǎng)絡(luò)中有若干路由器，上面運(yùn)行著OLSR路由協(xié)議。每個(gè)路由器維護(hù)著各自的鏈路信息、鄰居信息、拓?fù)湫畔⒑吐酚尚畔⒌?。為簡化模型，這里只考慮鏈路信息。LinkSet是鏈路信息的集合，路由器通過LinkSet維護(hù)鏈路信息。每條鏈路信息就是一個(gè)五元組linkTuple:=。其中：L_local_iface_addr表示路由器的本地接口地址；L_neigh_iface_addr表示與此路由器通信的鄰居路由器的接口地址；L_SYM_time表示鏈路狀態(tài)是雙向的生存時(shí)間；L_ASYM_time表示鏈路狀態(tài)是單向的生存時(shí)間；L_time表示元組的生存時(shí)間。當(dāng)L_time的生存期滿之后，整個(gè)元組將被刪掉，表示這條鏈路已不再可用。L_SYM_time在生存期內(nèi)意味著L_local_iface_addr和L_neigh_iface_addr之間的連接是雙向的，即任意一方均可收到對方發(fā)來的消息，而其生存期滿意味著L_local_iface_addr和L_neigh_iface_addr之間的連接不再是雙向的，即可能是單向的或者已經(jīng)斷開。L_ASYM_time在生存期內(nèi)意味著L_local_iface_addr可以接收到來自L_neigh_iface_addr的數(shù)據(jù)，而其生存期滿意味著L_local_iface_addr和L_neigh_iface_addr之間已經(jīng)斷開連接。

一個(gè)元組就是一條定時(shí)數(shù)據(jù)。路由器維護(hù)的鏈路集中的多個(gè)元組構(gòu)成一組難以建模的復(fù)雜定時(shí)數(shù)據(jù)。

2.2 原有建模模板的局限

2.2.1 同步定時(shí)數(shù)據(jù)建模模板

系統(tǒng)更新過的數(shù)據(jù)在一定生存時(shí)間后會失效。系統(tǒng)會在數(shù)據(jù)失效時(shí)，將這組數(shù)據(jù)刪除。這類系統(tǒng)的例子有電梯系統(tǒng)、ATM機(jī)系統(tǒng)和一個(gè)分析轉(zhuǎn)盤系統(tǒng)[8]等。其特點(diǎn)是數(shù)據(jù)可在任意時(shí)刻到達(dá)，但只在一段時(shí)間內(nèi)有效，下次被激活的時(shí)間并不固定(見圖1)。

圖1 一組同步定時(shí)數(shù)據(jù)的建模方法

這種方法可以方便地管理系統(tǒng)中的同步定時(shí)數(shù)據(jù)。但對于OLSR協(xié)議的建模與驗(yàn)證問題來說，這種建模模板太簡單，無法全面描述各節(jié)點(diǎn)的中間信息。

2.2.2 周期性更新的定時(shí)數(shù)據(jù)建模模板

多條數(shù)據(jù)的有效期相同并且只在特定的時(shí)鐘周期上改變值或有效性，如實(shí)時(shí)監(jiān)測溫度和濕度信息的輪詢系統(tǒng)等。其特點(diǎn)是數(shù)據(jù)周期性地發(fā)生變化。上面提到的建模方法就顯得非常復(fù)雜，在變量個(gè)數(shù)不確定的情況下(比如網(wǎng)絡(luò)和系統(tǒng)交互時(shí)的中間信息)，甚至?xí)o法建模。這類系統(tǒng)如圖2所示。

圖2 相同有效期變量的建模

這種建模方法即使做了擴(kuò)展，仍然不能對OLSR協(xié)議中的數(shù)據(jù)結(jié)構(gòu)建模，因?yàn)镺LSR協(xié)議的數(shù)據(jù)可以在任意時(shí)刻發(fā)生變化，并不會局限在固定的時(shí)鐘周期上。

3 復(fù)雜定時(shí)數(shù)據(jù)建模的方法

對帶有復(fù)雜定時(shí)數(shù)據(jù)的系統(tǒng)來說，通常對時(shí)間的建模是內(nèi)嵌在模型里的，若各條數(shù)據(jù)結(jié)構(gòu)都含有生存時(shí)間，即數(shù)據(jù)有效性會在定時(shí)器到期時(shí)發(fā)生變化，則通常的建模方法會變得相當(dāng)復(fù)雜；若多條數(shù)據(jù)結(jié)構(gòu)中都含有獨(dú)立的生存時(shí)間，則普通的方法完全無法正確建模。

在路由協(xié)議中，多個(gè)節(jié)點(diǎn)可能在任意時(shí)刻發(fā)起通信，并在接收到消息包后更新各自的局部變量。其中復(fù)雜定時(shí)數(shù)據(jù)的特點(diǎn)是多條數(shù)據(jù)的有效期是固定的時(shí)間段，但對這些數(shù)據(jù)進(jìn)行的更新可能發(fā)生在任意時(shí)刻。因?yàn)閁PPAAL工具沒有提供類似定時(shí)器變量的機(jī)制，故難以精確地刻畫變量的生存時(shí)間，但可以采用非精確的時(shí)間分片策略來取得結(jié)果。這種方法借鑒了早期計(jì)算機(jī)操作系統(tǒng)中的忙等方法，即每隔一段時(shí)間檢查一下變量，并更新數(shù)據(jù)的生存時(shí)間。這種情形下的建模模板如圖3所示。圖3(a)中的自動(dòng)機(jī)是更新自動(dòng)機(jī)，負(fù)責(zé)每過一個(gè)時(shí)間片對數(shù)據(jù)的有效性進(jìn)行一次檢查。這個(gè)檢查過程獨(dú)立于發(fā)送周期和各自的生存周期。在checkTime()函數(shù)所在的邊上加入條件x

圖3 復(fù)雜定時(shí)變量的建模

在圖3所示的模型中，由于對數(shù)據(jù)生存時(shí)間的更新只能發(fā)生在INTERVAL的倍數(shù)時(shí)間上，故而所提出的方法能表示的精度有限，即精度為INTERVAL。這種表示方法雖然有精度上的缺陷，但卻不影響對OLSR路由協(xié)議的驗(yàn)證，其原因在于，OLSR協(xié)議中的每個(gè)節(jié)點(diǎn)對鏈路信息都有一個(gè)保持時(shí)間(HOLD TIME)，當(dāng)發(fā)現(xiàn)鏈路斷開后，還要經(jīng)過一個(gè)保持時(shí)間，鏈路才會真正斷開。保持時(shí)間通常和HELLO的發(fā)送周期相同，并且模型中又忽略了鏈路丟包的情形，故只需INTERVAL的值相對于保持時(shí)間來說較小，即可保證時(shí)間片的精度不會影響所需驗(yàn)證的原系統(tǒng)的重要性質(zhì)。因此，這種方法的誤差不至于導(dǎo)致協(xié)議主要性質(zhì)的改變。

在復(fù)雜定時(shí)變量建模方法中，每隔一小段時(shí)間必須檢查一次變量，使得系統(tǒng)增加大量的額外操作。若設(shè)置的時(shí)間間隔過小，則驗(yàn)證耗時(shí)會成倍增長，時(shí)間代價(jià)會非常巨大。為了兼顧精確度和時(shí)間代價(jià)，通常選擇INTERVAL為HOLD_TIME的五分之一到三分之一。

4 建模方法的應(yīng)用

本文以O(shè)LSR協(xié)議中HELLO消息的傳輸和存儲為應(yīng)用背景，以鏈路信息為例，驗(yàn)證協(xié)議的鏈路保持功能和對鏈路斷開的敏感性。選擇的系統(tǒng)是一個(gè)運(yùn)行OLSR協(xié)議的網(wǎng)絡(luò)，有6個(gè)運(yùn)行OLSR協(xié)議的節(jié)點(diǎn)。一個(gè)節(jié)點(diǎn)的行為用一個(gè)自動(dòng)機(jī)描述，用一個(gè)自動(dòng)機(jī)判斷網(wǎng)絡(luò)是否收斂，并在網(wǎng)絡(luò)收斂后控制一條鏈路斷開，再讓此自動(dòng)機(jī)處于另一個(gè)位置，最后根據(jù)此位置驗(yàn)證節(jié)點(diǎn)對鏈路斷開的敏感性。使用本文提出的方法為各節(jié)點(diǎn)的鏈路信息建模，建模結(jié)果如圖4所示。6個(gè)自動(dòng)機(jī)分別模擬了各個(gè)節(jié)點(diǎn)。

圖4 OLSR協(xié)議中的鏈路信息示例模型

為了驗(yàn)證圖4所示模型對鏈路中斷的敏感性,本文采用如下兩條性質(zhì)：

(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)

這條性質(zhì)指在網(wǎng)絡(luò)收斂后，若1和3之間的鏈路斷開，則在本地信息中的鏈路將繼續(xù)保留HOLD_TIME-INTERVAL個(gè)時(shí)間單位。

(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)

這條性質(zhì)是指在網(wǎng)絡(luò)收斂后，若node_A和node_B之間的鏈路斷開，且時(shí)間超過HOLD_TIME個(gè)時(shí)間單位，則在本地鏈路信息中顯示node_A和node_B之間的鏈路已被刪除。

驗(yàn)證所采用的平臺為聯(lián)想ThinkStation D20，12G內(nèi)存，3.07GHz *19英特爾Xeon CPU，64位Ubuntu12.04 操作系統(tǒng)。驗(yàn)證結(jié)果如圖5所示，表明模型較好地描述了原系統(tǒng)。

圖5 示例模型的驗(yàn)證結(jié)果

5 結(jié) 語

本文解決了采用模型檢測技術(shù)驗(yàn)證路由協(xié)議的建模難題。對路由協(xié)議中的復(fù)雜定時(shí)數(shù)據(jù)建模，本質(zhì)上是為數(shù)據(jù)有效性隨時(shí)間變化的行為進(jìn)行建模。本文提出的方法首先對數(shù)據(jù)的生存時(shí)間進(jìn)行離散化處理，然后通過得到的時(shí)間分片對生存時(shí)限進(jìn)行建模，最后由管理自動(dòng)機(jī)進(jìn)行統(tǒng)一管理，從而解決復(fù)雜定時(shí)數(shù)據(jù)的建模難題。對OLSR協(xié)議的鏈路保持功能進(jìn)行驗(yàn)證的結(jié)果表明，本文提出的方法可以有效地對復(fù)雜定時(shí)數(shù)據(jù)建模。本文提出的方法可在網(wǎng)絡(luò)協(xié)議的驗(yàn)證過程中滿足要求，但對于時(shí)間精度要求更高的實(shí)時(shí)系統(tǒng)，其精度問題仍會影響系統(tǒng)的重要性質(zhì)。另外，大量的空轉(zhuǎn)操作嚴(yán)重影響驗(yàn)證的性能。

下一步的研究是進(jìn)一步細(xì)化此建模方法，以便在精度和時(shí)間代價(jià)上取得更好的平衡。并且，針對時(shí)間間隔過短造成的驗(yàn)證時(shí)間急劇增加問題，重點(diǎn)研究精確加速技術(shù)，以便在高驗(yàn)證精度之下加快驗(yàn)證速度。

參考文獻(xiàn):

[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.