時(shí)間自動(dòng)機(jī)模型的安全計(jì)算機(jī)平臺(tái)的形式化驗(yàn)證分析

摘要：越來越多的工業(yè)領(lǐng)域?qū)τ?jì)算機(jī)控制系統(tǒng)的可用性、可靠性和安全性要求越來越嚴(yán)格，而2乘2取2冗余結(jié)的計(jì)算機(jī)平臺(tái)正是解決這一問題的一種重要方式。本文通過分析CBTC系統(tǒng)安全計(jì)算機(jī)平臺(tái)各組成結(jié)構(gòu)的基礎(chǔ)上，提取出了時(shí)間自動(dòng)機(jī)的校驗(yàn)助手UPPAAL，并通過建立一個(gè)系統(tǒng)模型，在此基礎(chǔ)上再進(jìn)行驗(yàn)證和分析。

關(guān)鍵詞：計(jì)算機(jī)；時(shí)間自動(dòng)機(jī)；模型驗(yàn)證

中圖分類號(hào)：TP301.1 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號(hào)：1674-7712 （2012） 18-0049-01

一、時(shí)間自動(dòng)機(jī)和它的驗(yàn)證助手UPPAAL

Alur創(chuàng)立了時(shí)間自動(dòng)機(jī)，它被稱為一種計(jì)算模型，能夠充分地描述系統(tǒng)的行為。一個(gè)一個(gè)的時(shí)間自動(dòng)機(jī)TA1，…，TA通過并行的復(fù)合就構(gòu)成了時(shí)間自動(dòng)機(jī)的網(wǎng)絡(luò)，每個(gè)TAi（1≤i≤n）稱為時(shí)間自動(dòng)機(jī)的每一個(gè)進(jìn)程，所有這些進(jìn)程的通信是通過通道或共享全局變量的方式而實(shí)現(xiàn)的，同步通信的實(shí)現(xiàn)是以運(yùn)用輸入和輸出動(dòng)作而獲得握手同步的方式，異步通信的實(shí)現(xiàn)是以共享全局變量的方式。要想真正實(shí)現(xiàn)模擬握手同步這一目標(biāo)，時(shí)間自動(dòng)機(jī)在標(biāo)記中主要含有兩個(gè)動(dòng)作符號(hào)，即輸入的符號(hào)a？和輸出的符號(hào)a！。

時(shí)間自動(dòng)機(jī)的驗(yàn)證助手UPPAAL是一個(gè)為集成的實(shí)時(shí)系統(tǒng)提供建模和驗(yàn)證環(huán)境情況的助手，可以在此適用敘述成不確定的并行過程的積的系統(tǒng)。每一個(gè)過程都可以理解為由實(shí)數(shù)值時(shí)鐘、變量和有限控制的結(jié)構(gòu)而構(gòu)成的時(shí)間自動(dòng)機(jī)，過程之間通信的實(shí)現(xiàn)是利用管道和共享的變量而實(shí)施的，管道的最大益處是可以使不同的自動(dòng)機(jī)中的兩個(gè)轉(zhuǎn)換能夠一塊進(jìn)行。在建立一個(gè)比較完整的性質(zhì)自動(dòng)機(jī)和系統(tǒng)自動(dòng)機(jī)后，才可以對(duì)自動(dòng)機(jī)理論的模型檢驗(yàn)方法進(jìn)行驗(yàn)證，UPPAAL采用了一種稱為“on-the-fly”的搜索技巧，在跟性質(zhì)自動(dòng)機(jī)的乘積相判空的情況下，如果有需要，系統(tǒng)自動(dòng)機(jī)的狀態(tài)就可以生成了，如此是不需要為系統(tǒng)建立全部的狀態(tài)空間，這樣就使模型驗(yàn)證器的效率得以提高。

二、時(shí)間自動(dòng)機(jī)的系統(tǒng)建模

（一）系統(tǒng)的結(jié)構(gòu)和功能。由容錯(cuò)安全管理（FTSM）單元和6臺(tái)工控機(jī)組成了安全計(jì)算機(jī)平臺(tái)的系統(tǒng)，它一共分成了3個(gè)模塊，如圖1所示。

每個(gè)模塊的組成和功能有：

1.處理單元模塊：2乘2取2的結(jié)構(gòu)是由4臺(tái)工控機(jī)組成的，4臺(tái)工控機(jī)各自叫做處理單元的PUA1、PUA2、PUB1、PUB2，其中，2取2結(jié)構(gòu)的通道A是由PUA1與PUA2、PUB1與PUB2組成的，通道B的作用是在處理的結(jié)果輸出至數(shù)據(jù)輸入輸出模塊之前，處理輸入數(shù)據(jù)。

2.數(shù)據(jù)輸入輸出的模塊：它是由兩臺(tái)工控機(jī)構(gòu)成的負(fù)責(zé)輸入輸出數(shù)據(jù)轉(zhuǎn)發(fā)的。

3.安全表決模塊：它是由兩個(gè)容錯(cuò)的安全管理單元FTSMA和FTSMB組成，可以實(shí)時(shí)檢測(cè)數(shù)據(jù)輸入輸出的模塊和處理單元的模塊的6臺(tái)工控機(jī)。表決通道A、B的主備狀態(tài)的切換可以在此進(jìn)行，還可以對(duì)通信控制器的狀態(tài)進(jìn)行控制。

4.2取2的通道之間的切換：這兩個(gè)通道的狀態(tài)模式主要有斷電模式、狀態(tài)模式、跟隨模式、上電模式、備通道模式和主通道模式。

（二）通道內(nèi)2取2雙機(jī)的同時(shí)進(jìn)行。在通道內(nèi)2取2雙機(jī)的工作流程之間的同時(shí)進(jìn)行關(guān)系不是很寬松的。一定要在第三方的FTSM單元進(jìn)行判決后，才能夠?qū)嵭?取2雙機(jī)的同時(shí)進(jìn)行，一定要在相同的時(shí)間間隔內(nèi)確保FTSM的單元部分收到雙機(jī)的同時(shí)進(jìn)行的提示，同時(shí)進(jìn)行被判定成功后，及時(shí)告知要求同時(shí)進(jìn)行的雙方獲取同時(shí)進(jìn)行的成功；如果ISM的單元部分在同時(shí)進(jìn)行的時(shí)間間隔之內(nèi)沒有獲得相應(yīng)的同時(shí)進(jìn)行的要求，就能認(rèn)為雙機(jī)的同時(shí)進(jìn)行是失敗的。電的初始同時(shí)進(jìn)行的時(shí)間范圍要求在480個(gè)單位之內(nèi)，處理單元時(shí)的操作周期卻是340個(gè)單位，一共可以分成4個(gè)微周期，即正常的同時(shí)進(jìn)行的周期，輸入數(shù)據(jù)的周期，ZC應(yīng)用的周期和輸出數(shù)據(jù)的周期，同時(shí)進(jìn)行的時(shí)間各自為20、60、200、60個(gè)時(shí)間單位。在處理的單元部分上，如果存在一步的FTSM認(rèn)定為雙機(jī)不能夠同時(shí)進(jìn)行，這是就要重新開啟處理的單元PU1，PU2，于此同時(shí)，F(xiàn)TSM也就進(jìn)入了一個(gè)初始的狀態(tài)。

三、驗(yàn)證過程分析

在驗(yàn)證的時(shí)候，就會(huì)出現(xiàn)一些在設(shè)計(jì)上不夠合理的位置。比如，F(xiàn)TSM規(guī)定在通道內(nèi)的雙機(jī)的同時(shí)進(jìn)行的時(shí)間間隔是各微周期的時(shí)間長(zhǎng)度，也就是說雙機(jī)同時(shí)進(jìn)行的時(shí)差最大的值是每個(gè)微周期的時(shí)間長(zhǎng)度，這種現(xiàn)象是不合乎邏輯的。用輸入數(shù)據(jù)的微周期為一個(gè)例子，它的驗(yàn)證

語句是：

雙機(jī)的同時(shí)進(jìn)行的時(shí)間限制是每個(gè)微周期的時(shí)間長(zhǎng)度：

A[]（ftsmA.DatalnDoneimPly（timerAI一timerAZ）<=60 and（timerAI-

timerAZ）>=一60）.

雙機(jī)同時(shí)進(jìn)行的時(shí)間差的最大值是每個(gè)微周期的時(shí)間長(zhǎng)度：

E<>（ftSInA.DatalnDoneand（timerAI一timerAZ）==60）

A[]not（ftsmA.DatalnDoneand（timerAI一timerAZ）==61）

查看安全計(jì)算機(jī)平臺(tái)系統(tǒng)運(yùn)行的測(cè)試記錄，發(fā)現(xiàn)的確存在微周期內(nèi)雙機(jī)同時(shí)進(jìn)行但是時(shí)差很大的情況。例如，如果輸入數(shù)據(jù)微周期的時(shí)間長(zhǎng)度是60個(gè)時(shí)間單位，而雙機(jī)請(qǐng)求同時(shí)進(jìn)行的時(shí)間分別是20和50個(gè)時(shí)間單位。在雙機(jī)的硬件相同，并且晶振、通信延時(shí)等誤差源的數(shù)量級(jí)相比要小很多，是不能忽略這么大的時(shí)差的，這就說明系統(tǒng)的危險(xiǎn)隨時(shí)都有可能發(fā)生，比如，處理單元CPU出現(xiàn)降頻處理和單元硬件出現(xiàn)故障等。在設(shè)計(jì)新一版的平臺(tái)系統(tǒng)中，將會(huì)限定雙機(jī)同時(shí)進(jìn)行的時(shí)間差值，在把第一個(gè)微周期，即正常同時(shí)進(jìn)行的微周期取消后，對(duì)剩下的三個(gè)微周期設(shè)定同時(shí)進(jìn)行時(shí)間的閾值，超出閾值則判定為雙機(jī)同時(shí)進(jìn)行失敗，這樣就保證了每個(gè)微周期的同時(shí)進(jìn)行。

參考文獻(xiàn)：

[1]朱維軍，王迤冉，周清雷.時(shí)間自動(dòng)機(jī)模型驗(yàn)證的研究進(jìn)展[J].計(jì)算機(jī)應(yīng)用與軟件，2008，6.

[2]張宏韜.基于閉塞時(shí)間模型的城市軌道交通運(yùn)輸能力研究[D].北京交通大學(xué)，2012.

[3]徐曉燕，陳文賽.一種用于軌道交通的安全計(jì)算機(jī)平臺(tái)的設(shè)計(jì)與實(shí)現(xiàn)[J].信息化研究，2009，8.