基于B/S架構(gòu)的實時系統(tǒng)建模驗證工具

石 安 張卓若 代立云

(西南大學(xué) 重慶 400715)

0 引 言

近年來，科學(xué)技術(shù)迅猛發(fā)展，對嵌入式實時系統(tǒng)應(yīng)用的需求不斷增加，實時系統(tǒng)(Real-time System)在核研究、航空航天、軍事和民用領(lǐng)域都有著廣泛的作用，如核反應(yīng)冷卻系統(tǒng)、過程控制系統(tǒng)、交通控制系統(tǒng)、軌道信號系統(tǒng)等。實時系統(tǒng)計算結(jié)果的正確性是指在規(guī)定時間內(nèi)做出正確的程序邏輯響應(yīng)。即系統(tǒng)須及時響應(yīng)外部條件的要求，控制所有實時設(shè)備和實時任務(wù)在指定或確定的時間內(nèi)協(xié)調(diào)一致地運行，完成系統(tǒng)功能。因此，實時系統(tǒng)需要在預(yù)定義的時間內(nèi)對事件進行相應(yīng)的處理與反饋。若該實時系統(tǒng)無法滿足在“可執(zhí)行時間”“任務(wù)周期”“通信延時”等方面的特定時間約束，可能會引發(fā)重大錯誤和安全隱患。如何有效地保證設(shè)計實時系統(tǒng)的安全性和可靠性，并保證各子系統(tǒng)的正常交互和各子任務(wù)的協(xié)調(diào)一致，一直是設(shè)計開發(fā)人員所關(guān)注的重點和難點。為了滿足開發(fā)人員對實時系統(tǒng)的開發(fā)需求，基于現(xiàn)有建模與驗證工具UPPAAL的優(yōu)缺點，在繼承其高可靠性與實時性優(yōu)點的同時，克服其下載安裝慢、拖拽控件不靈活且不支持多用戶進行項目團隊管理的缺點，本文設(shè)計實現(xiàn)了基于B/S架構(gòu)的實時系統(tǒng)建模與驗證工具。

1 相關(guān)背景

近年來，實時系統(tǒng)復(fù)雜性不斷提高，硬件、軟件規(guī)模不斷增大。同時，實時系統(tǒng)具備的外部環(huán)境和系統(tǒng)內(nèi)部的交互性、多種類型任務(wù)的混合性及對時間約束的嚴格性等，更增加了對其分析和驗證的難度。從實時系統(tǒng)領(lǐng)域中應(yīng)用的形式化方法來看，在計算機系統(tǒng)上層規(guī)范到最終實現(xiàn)的過程中，使用形式化語言對系統(tǒng)需求進行描述，并選擇適當?shù)男问交ぞ哌M行系統(tǒng)輔助設(shè)計和安全性驗證，能夠在較大程度上減少由系統(tǒng)開發(fā)人員引起的設(shè)計失誤，從而提高系統(tǒng)的安全性[1-2]。

1.1 形式化方法

通俗地講，形式化方法即通過數(shù)學(xué)邏輯的手段設(shè)計并開發(fā)一個高可靠性的系統(tǒng)。與傳統(tǒng)的軟件開發(fā)方法不同，形式化方法更加偏向于理論。國內(nèi)外研究機構(gòu)和學(xué)者根據(jù)各自不同的背景和研究基礎(chǔ)，提出了眾多形式化模型和驗證方法。其中，模型檢驗(Model Checking)[3-4]是一種常用的實時系統(tǒng)形式化驗證方法，在工業(yè)領(lǐng)域得到了較為廣泛的應(yīng)用。模型檢驗方法最早由Clarke等[5]及Quielle等[6]分別提出，使用狀態(tài)空間搜索的方法遍歷根據(jù)系統(tǒng)規(guī)范而設(shè)計的實現(xiàn)模型，系統(tǒng)的規(guī)范(Specification)由一種形式語言描述，從而進一步檢驗該計算模型是否滿足某條由時態(tài)邏輯(Temporal Logic)公式所表示的特定性質(zhì)。該方法可將驗證過程自動化，即容易采用計算機進行輔助驗證，應(yīng)用起來比較簡便，對工程技術(shù)人員的理論要求不高；同時，模型檢驗技術(shù)可對設(shè)計模型中的錯誤進行定位，當系統(tǒng)性質(zhì)未被滿足時可給出反例，幫助用戶發(fā)現(xiàn)錯誤，增加了系統(tǒng)安全設(shè)計的可用性。但鑒于實時系統(tǒng)中時間變量的無界性，系統(tǒng)復(fù)雜性的提高易導(dǎo)致模型驗證過程中出現(xiàn)狀態(tài)爆炸問題。

1.2 同類系統(tǒng)研究應(yīng)用與現(xiàn)狀

近年來，國內(nèi)外在實時系統(tǒng)的建模驗證工作上取得了較大的進展，并推出了相應(yīng)的算法和工具，包括改進的SMV[7]、AT&T的基于自動機理論的典型模型檢驗工具SPIN[8-9]、UPPAAL[10]等。其中，UPPAAL由于其可靠性和實時性高，是目前使用最為廣泛的實時系統(tǒng)建模驗證工具。UPPAAL是一個集成的工具環(huán)境，將時態(tài)邏輯模型檢測理論及時間自動機理論相互結(jié)合，目前已大量應(yīng)用于對實時控制器和通信協(xié)議的描述和驗證[11]。UPPAAL使用快速驗證技術(shù)和限制技術(shù)等模型驗證技術(shù)，從而有效地保證了實時系統(tǒng)的安全性和正確性，同時還解決狀態(tài)空間爆炸問題。UPPAAL主要包含系統(tǒng)編輯器(System Editor)、驗證器(Verifier)、模擬器(Simulator)三部分。盡管功能已較為成熟，UPPAAL同樣存在一些弊端。作為一款桌面應(yīng)用程序，其需要從官網(wǎng)上填寫個人信息后下載安裝，等待時間較長；此后如有版本的更新，用戶亦需另行下載新版軟件。且局限于其JAR文件格式，用戶需要配置Java運行環(huán)境和較高版本的JDK。同時，UPPAAL的用戶界面設(shè)定有所欠缺，一些控件的點擊、拖拽并不十分靈活，使得其在效率、有效性和用戶體驗等方面降低了性能。此外，UPPAAL的單用戶設(shè)計不適合項目團隊管理。更為重要的是，UPPAAL作為20世紀90年代誕生的一款工具軟件，其后續(xù)所有版本的設(shè)計思想還停留在單機應(yīng)用程序的構(gòu)建思路上，早已落后于當前應(yīng)用軟件形態(tài)逐漸向網(wǎng)絡(luò)化、服務(wù)化、云化發(fā)展的未來趨勢，需要對其從系統(tǒng)架構(gòu)上實施全面的改造和重新開發(fā)。

基于對實時系統(tǒng)建模驗證工具的需求，同時結(jié)合現(xiàn)有相關(guān)工具存在的問題，本次系統(tǒng)在同樣保證實時系統(tǒng)檢驗的安全性和正確性的前提下，采用B/S架構(gòu)使得驗證工具具有更簡潔美觀的用戶界面且可以免安裝直接在瀏覽器打開鏈接后使用，更快捷的同時，減少軟件對電腦硬盤容量的占用和運行時對內(nèi)存的消耗。而且B/S架構(gòu)也能更便捷地擴展到項目的團隊上。在保證程序升級方便，維護成本低的同時，能夠在兼容性、可理解性、可用性等方面帶給用戶更友好的體驗。這不僅對于這類工具本身的生長演化極具意義，更有利于向從事基于時間自動機的實時系統(tǒng)分析與驗證領(lǐng)域研究的學(xué)者提供一款具備高可用性、高效率、輕量級、低成本的工具。

2 系統(tǒng)設(shè)置

本次系統(tǒng)開發(fā)前端使用mxGraph框架，通過JS實現(xiàn)網(wǎng)頁界面和相關(guān)數(shù)據(jù)的顯示，后端使用Java進行相關(guān)驗證性任務(wù)的實現(xiàn)，前后端之間使用Ajax進行數(shù)據(jù)的傳輸。整個系統(tǒng)主要實現(xiàn)在線編輯時間自動機模型并對其相關(guān)性質(zhì)進行驗證，并且對于驗證的結(jié)果會有反饋信息的顯示。滿足實時系統(tǒng)開發(fā)過程中，對于時間自動機模型的驗證需求。在保證響應(yīng)速度的同時，提供準確的驗證結(jié)果。

2.1 架構(gòu)設(shè)計

為實現(xiàn)上述功能，基于B/S架構(gòu)進行設(shè)計與開發(fā)。用戶通過瀏覽器進入操作界面，將大部分的事務(wù)邏輯留在后端實現(xiàn)。將Web瀏覽器作為核心應(yīng)用軟件，后端負責實現(xiàn)功能的關(guān)鍵部分，這樣既利于開發(fā)又便于后期維護和用戶使用。系統(tǒng)整體架構(gòu)設(shè)計如圖1所示。

2.2 整體功能設(shè)計

系統(tǒng)前端需要實現(xiàn)相關(guān)時間自動機模型的建模，包括圖模型的導(dǎo)入導(dǎo)出，編輯和相關(guān)數(shù)據(jù)的處理與展示。在完成一個完整的時間自動機模型的生成之后，可以驗證其相關(guān)性質(zhì)并在前端返回驗證結(jié)果，驗證等相關(guān)功能的實現(xiàn)集中于后端。前后端之間的數(shù)據(jù)傳輸，采用Ajax技術(shù)，保證數(shù)據(jù)傳輸?shù)男?，從而提高整個系統(tǒng)在驗證過程中的響應(yīng)速度。系統(tǒng)整體的功能流程如圖2所示。

2.3 具體功能實現(xiàn)

mxGraph框架將圖表元素的屬性和圖元間關(guān)聯(lián)關(guān)系的描述以XML的格式保存和進行數(shù)據(jù)交換，能夠?qū)⒂脩羲庉媹D形的數(shù)據(jù)存儲成XML文件；此后，可快捷方便地通過Ajax傳遞到后端Servlet，將mxGraph生成的XML文件轉(zhuǎn)換成UPPAAL格式的XML文件，然后通過命令行的方式連接到調(diào)用Verifyta驗證器進行檢驗。檢驗的結(jié)果又通過Ajax返回到前端進行顯示。

2.3.1前端mxGraph的使用

前端使用JS編寫，結(jié)合mxGraph框架并生成XML文件。mxGraph是一個開源的JavaScript繪圖組件，其前身為2000年推出的JGraph[12]。mxGraph主要提供快速生成可視化的圖表、對圖表進行自動化的布局、排列和分析，并提供相應(yīng)的用戶交互等功能[12]。在開發(fā)實現(xiàn)網(wǎng)頁編輯顯示W(wǎng)orkflow/BPM流程圖、網(wǎng)絡(luò)拓撲圖和普通圖形等的Web應(yīng)用程序過程中常涉及mxGraph框架相關(guān)技術(shù)。該框架具備架構(gòu)簡單、兼容性高、有效靈活的圖像可視化等優(yōu)點，可以很好地滿足本次系統(tǒng)開發(fā)在前端對于圖形高效編輯的需求。利用mxGraph中內(nèi)置的文件字符解碼器，可以方便地將格式內(nèi)容精簡且易于解析的XML格式文檔轉(zhuǎn)換為用戶所需的數(shù)據(jù)格式文件。所支持的文件格式的存儲包括GIF、JPG、PDF、SVG等，用戶可根據(jù)實際需要靈活進行文件格式的選取。

2.3.2Ajax的使用

Ajax(Asynchronous JavaScript and XML)，即異步的JavaScript和XML，能夠與服務(wù)器進行數(shù)據(jù)交換，并具有能夠在不需要重新更新整個頁面的情況下，只更新發(fā)生了數(shù)據(jù)改變的部分網(wǎng)頁的功能。使用Ajax技術(shù)進行前端和后端的數(shù)據(jù)傳輸，實現(xiàn)導(dǎo)出XML文件、保存圖片等，以及進行條件的驗證等，同時將結(jié)果返回給用戶。同時，在異步調(diào)用時通過設(shè)置請求超時處理，當數(shù)據(jù)請求失敗時在頁面提示用戶檢查網(wǎng)絡(luò)或者數(shù)據(jù)庫連接情況，提供了操作友好的人機交互[14]。如此使得Web應(yīng)用程序更為迅捷地響應(yīng)用戶交互，實現(xiàn)了網(wǎng)頁與網(wǎng)頁間的平滑過渡，縮短用戶等待時間，提升了用戶體驗。此外，Ajax采用異步方法與服務(wù)器通信，在不打斷用戶操作的前提下，通過降低網(wǎng)絡(luò)數(shù)據(jù)流量且提高數(shù)據(jù)傳輸效率，優(yōu)化了瀏覽器和服務(wù)器之間的溝通。

2.3.3后端Servlet的使用

后端使用Servlet可接收Ajax傳來的請求，并實現(xiàn)將前端用戶編輯并顯示的圖形導(dǎo)出PDF、JPG、PNG、XML等格式文件輸出；將mxGraph格式的XML文件轉(zhuǎn)化成UPPAAL格式的XML文件；連接verifyta進行某條件的形式化檢驗等功能。此外，可通過Servlet實現(xiàn)包括數(shù)據(jù)壓縮、Web和URL訪問、圖像處理、JDBC、多線程等功能。

2.3.4Verifyta的使用

后端Servlet通過相關(guān)命令行語句的調(diào)用，連接到Verifyta，實現(xiàn)對程序可達性、安全性、活性等性質(zhì)的驗證。

UPPAAL的Verifyta驗證器可由命令行調(diào)用，進行驗證條件(Property)的形式化檢驗，輸出結(jié)果(Satsified、Unsatisfied、Error)并在條件不滿足時生成反例軌跡(Counter-example)到xtr文件(UPPAAL的歷史執(zhí)行軌跡文件)。

3 系統(tǒng)實現(xiàn)

3.1 系統(tǒng)編輯器的原理和構(gòu)成

單擊并展開左側(cè)邊欄中“Timed Automata”選項，可將長方形表示的模版和圓形表示的位置拖入右側(cè)畫面。系統(tǒng)最右側(cè)顯示圖的相關(guān)屬性，除常規(guī)的圖的相關(guān)屬性設(shè)置之外，還包括時間自動機的相關(guān)參數(shù)設(shè)置、函數(shù)聲明等。

雙擊模版，即可進行模版的定義。模版(Templates)具有唯一確定的名稱(Name)、模版聲明(Declaration)和模版參數(shù)(Parameter)。其中，模版聲明的變量為僅可供該模版使用的局部變量和時鐘變量；模版參數(shù)可以是int、chan、const等類型的符號變量或常量(Symbolic variables and Constants)，進程聲明(Process Declaration)時被賦值。由于系統(tǒng)通常具有多個相似的進程(Process)，通過定義模版(Templates)并在實例化時更改相應(yīng)參數(shù)等，即可同時生成多個進程。系統(tǒng)主界面如圖3所示。

點擊右側(cè)邊欄“Edit Declaration”按鈕，彈出框分別包含“Declaration”“Property”“Instantiation”選項。其中：“Declaration”中進行全局的時鐘、整型、通道等類型變量的聲明，在此中聲明的變量在所有Template中有效共享；“Property”中，用戶編輯、增刪驗證條件，并以此檢驗系統(tǒng)的行為和性質(zhì)；“Instantiation”中對模版進行實例化，生成相應(yīng)進程。點擊圖的頂點和邊也可以進行相關(guān)屬性的設(shè)置，頂點和邊所包含的各自屬性及其含義如表1所示。

表1 頂點和邊相關(guān)屬性含義表

3.2 驗證器的原理和構(gòu)成

由于該程序的驗證部分使用了UPPAAL的verifyta驗證器，因此具體實現(xiàn)主要參照的UPPAAL中的運行方式。

TCTL支持A[]φ、E<>φ、A<>φ、E[]φ、φ→ψ等表達方式(φ和ψ表示狀態(tài)謂詞)，其路徑含義表如表2所示。

表2 路徑含義圖

查詢規(guī)范語言包括路徑公式(Path Formula)和狀態(tài)公式(Path Formula)。狀態(tài)公式是一個描述單個狀態(tài)的表達式，可表示某特定進程是否處于某個位置(Location)，如P1.cs and x<3，其中P1表示進程，cs表示位置；也可在不考慮模型行為的情況下對狀態(tài)進行評估，如x<3。

路徑公式量化模型的路徑或軌跡包括安全性(Saf-ety)、活性(Liveness)和可達性(Reachability)[17]，圖4描述了所支持的不同路徑公式。

可達性表示某給定公式φ是否能由某個可達到的狀態(tài)(Reachable State)滿足，即從初始狀態(tài)起，是否存在一條路徑可以最終達到某狀態(tài)，該狀態(tài)滿足公φ，表示為E[]φ?？蛇_性可以驗證模型的一些基本行為，但不能保證模型的正確性。

安全性即“某壞事永遠也不會發(fā)生”，指系統(tǒng)的正確性、互斥性和無死鎖性。在UPPAAL中，通過以A[]φ表示“某好事始終為真”，來驗證模型的安全性?；钚约础澳呈伦罱K一定會發(fā)生”，指系統(tǒng)的終止性、保證服務(wù)性和響應(yīng)性，可表示為A<>φ。考慮到前置條件時表示為φ→ψ，即一旦φ發(fā)生，ψ定會發(fā)生。

死鎖即證明系統(tǒng)在一般運行時不存在一個能夠循環(huán)執(zhí)行的路徑環(huán)。通過對每個狀態(tài)分別進行前向及后向搜索，如果都僅存在一條路徑能夠回到原來狀態(tài)，即認為存在該可循環(huán)執(zhí)行的路徑環(huán)。UPPAAL中使用公式A[] not deadlock表示全局是否存在死鎖狀態(tài)。

同時，對TCTL等實時時態(tài)邏輯公式進行模型檢驗時，須對狀態(tài)遷移的時間約束進行處理。在驗證系統(tǒng)響應(yīng)的實時性時，判斷某條件能否實現(xiàn)須搜索該響應(yīng)所有的可能路徑如可實現(xiàn)，則須繼續(xù)驗證時間約束能否被滿足，具體算法為把路徑上所有遷移的時間約束進行累加，計算所有路徑耗時的最大值，然后將該最大值和公式中的時間約束進行比較，從而判斷該系統(tǒng)響應(yīng)是否滿足實時性要求。

4 系統(tǒng)測試與實例分析

在完成了系統(tǒng)的開發(fā)之后，測試實例至關(guān)重要。此次測試采用了實時系統(tǒng)中常見的時間自動機模型實例，通過完整的建模與驗證流程來測試系統(tǒng)各個部分功能的實現(xiàn)情況。

4.1 Train-Gate實例簡介

Train-Gate被定義為由若干列火車和一個控制器組成的鐵路控制系統(tǒng)，描述列火車過橋的過程。該橋為一個共享的關(guān)鍵資源(Shared Critical Resource)，一次只可被其中一列火車訪問?；疖囃Ｏ潞椭匦聠佣夹枰獣r間。當火車靠近橋時，發(fā)出“appr！”信號，并在10 s內(nèi)監(jiān)聽控制器發(fā)來的停止信號“stop！”。如沒有接收到，則不停車，并在3～5 s內(nèi)通過，同時發(fā)送給控制器離開信號“l(fā)eave！”；如接收到，表示前面有其他火車正在通過該橋，則該列車停車?？刂破鹘邮盏健發(fā)eave？”信號，得知前一列火車離開橋后，會發(fā)出“go！”信號，通知正等待的火車中最前面的一列繼續(xù)行駛。該車收到信號后，有7～15 s的啟動時間，然后同樣在3～5 s內(nèi)通過該橋并發(fā)送“l(fā)eave！”信號。

4.2 過程演示

聲明全局變量。常量N表示火車數(shù)量。定義長度為N的typedef類型數(shù)組id_t作為模版train的參數(shù)。同時，分別定義長度為N的通道數(shù)組appr、stop、leave和緊急通道(Urgent Channel)。緊急通道表示啟動該轉(zhuǎn)換時，必須沒有延遲地同步執(zhí)行消息的傳遞。同時，模版聲明和全局聲明時，使用JavaScript的正則表達式，在前端進行語法檢驗，同時與用戶交互，進行相應(yīng)錯誤的提醒。即保證聲明的變量數(shù)據(jù)類型合法，為常量、整形、布爾型、通道類型、時鐘類型、typedef類型等；且各聲明語句之間由“；”隔開，從而更加確保生成相應(yīng)XML文件的正確性。全局變量聲明界面圖如圖5所示。

定義模版Train和Gate。將自動機中的頂點和邊的連接好后，進行相關(guān)屬性設(shè)置，完成建模。模板Train的自動機形式圖如圖6所示。

初始位置為Safe，可在任意時間到達Appr位置，此時通過appr[id]！通道，發(fā)送消息給Gate進程，并更新enqueue隊列的值，在其末尾添加此火車id號，表示該輛火車即將到達。

Appr位置具有不變量限制x≤20及兩種轉(zhuǎn)換選擇。其一，將轉(zhuǎn)向Stop位置，其保護條件為x≤10，并有名為stop[id]？的同步通道，表示在10 s內(nèi)某個不確定(Non-deterministic)時間，因接收到Gate進程通過Stop通道傳遞來的消息，跳轉(zhuǎn)到Stop位置。其二，將轉(zhuǎn)向Cross位置，其轉(zhuǎn)換條件為x≥10，更新公式為x=0，表示因一直未接收到Stop消息，在10 s到20 s內(nèi)的某個不確定時間，將跳轉(zhuǎn)到Cross位置，并將時鐘值重置為0。

Cross位置具有x≤5的不變量限制和x≥3，和通道leave[id]！，表示將在3～5 s某個時間，發(fā)送消息給Gate進程，并跳轉(zhuǎn)回初始位置Safe。如Gate進程處于Free位置，且滿足長度len>0，將跳轉(zhuǎn)到Occ位置；如處于Occ位置，將跳轉(zhuǎn)到Free位置，并將隊列中第一個元素彈出，表示第一列等待的火車。

Stop位置具有通道go[id]？和更新公式x=0，表示當收到Gate傳來的go消息后，將轉(zhuǎn)換到Start位置，并重置時鐘值為0。

Start位置具有不變量限制x≤15和x≥7，表示在7 s到15 s內(nèi)某時間到達Cross狀態(tài)。模板Gate的自動機形式圖如圖7所示。

Gate進程負責與train進程進行消息通信從而保證正在通過橋的火車只有一列。當Gate處于初始Free位置時，如隊列的長度len=0，表示此時沒有火車，則跳轉(zhuǎn)到Occ位置；如Gate處于Occ位置，則跳轉(zhuǎn)到下一緊急(Urgent)位置后，通過通道stop(tail())！，發(fā)送消息返回給該Train進程。

實例中Train模板和Gate模板的局部變量聲明和參數(shù)定義如圖8所示。

在圖8中，定義Train模版的局部時鐘變量x，并設(shè)置其參數(shù)id，值在0～5范圍。定義Gate模版的局部數(shù)組list，長度為N+1。同時定義局部函數(shù)enqueue()和dequeue()，分別表示在隊列l(wèi)ist的在末尾加入指定元素，或彈出其首部元素。

實例化Train和Gate模版為系統(tǒng)中的進程。在定義完成之后，必須進行聲明，完成實例化。即聲明了分別代表六列火車的六個Train類型的進程Train(0)-Train(5)，和一個Gate類型的進程。

在完成實例化以后，最終要檢驗該系統(tǒng)是否滿足相關(guān)性質(zhì)。四條消息分別從有無死鎖、可達性、安全性、活性等方面檢驗系統(tǒng)的正確性。性質(zhì)檢驗界面如圖9所示。

本例中具體檢驗條件內(nèi)容如下：

-A[] not deadlock 不存在死鎖。

-Train(0).Appr-->Train(0).Stop 每列靠近的火車，都會在通過橋之前先停止。此為故意設(shè)置的錯誤條件，用以檢驗系統(tǒng)對錯誤項的檢查和提示。

-A[]Train(0).Cross+Train(1).Cross+Train(2).Cross+Train(3).Cross+Train(4).Cross+Train(5).Cross<=1. 表明通過橋的一次只允許一列火車。(安全性)

-Train(0).Appr-->Train(0).Cross: 每列靠近橋的火車都會最終穿過該橋。保證最終所有火車都會順利通過該橋。(可達性)

在Property List中添加上述四個條件，并且在最后一行添加一個錯誤格式的條件，此處為人為故意設(shè)置的錯誤格式的驗證條件，從而檢驗系統(tǒng)能準確識別用戶輸入的是否是符合規(guī)范的檢驗性質(zhì)內(nèi)容。當條件滿足時，返回“Formula is Satisfied”；條件不滿足時返回“Formula is Not Satisfied”并提醒用戶在首頁面Tools-Trace中查看軌跡；此外，當輸入內(nèi)容錯誤時，會提示用戶“Input is Wrong”，以便提醒用戶在檢查所輸入的驗證性質(zhì)條件后重新輸入。測試結(jié)果顯示如圖10所示。

此案例中，在上文的檢驗條件具體內(nèi)容中可以看到，第二條性質(zhì)是故意設(shè)置為錯誤的性質(zhì)，故結(jié)果理應(yīng)是不滿足的。通過系統(tǒng)檢驗，得到了預(yù)期的正確結(jié)果，系統(tǒng)顯示第二條性質(zhì)不滿足，并且提示在Tools-Trace中顯示出反例軌跡。反例軌跡圖如圖11所示。

5 結(jié) 語

本文根據(jù)現(xiàn)實中科研人員在對于實時系統(tǒng)開發(fā)過程中，所遇到的時間自動機模型驗證的需求，設(shè)計并實現(xiàn)了一個基于B/S架構(gòu)的實時系統(tǒng)的建模與驗證工具，并通過測試一個經(jīng)典的Train和Gate時間自動機模型，實現(xiàn)其建模與性質(zhì)驗證，最終得到了預(yù)期的正確結(jié)果。

選擇基于B/S架構(gòu)更加符合當今網(wǎng)絡(luò)化、云化發(fā)展的趨勢。盡管本文基本達到了預(yù)期效果，但由于實時系統(tǒng)的驗證修正涉及到的領(lǐng)域廣泛且理論性強，在實際應(yīng)用中，為了達到更好的用戶體驗，需要對該驗證系統(tǒng)做進一步完善，通過建立用戶權(quán)限設(shè)定、限制文檔只讀可寫屬性、資源自定義加載和文檔本地自動保存及副本儲存與服務(wù)端上傳修改相結(jié)合等方式，可實現(xiàn)不同用戶對系統(tǒng)資源的訪問與修改，在不影響系統(tǒng)運行的安全性和可靠性的同時，實現(xiàn)資源的共享并提高工作效率。同時進一步提高驗證器的工作效率，改進相關(guān)驗證算法，滿足實時系統(tǒng)的建模和檢驗過程中更多需求，例如在圖11中還有兩處留出的更多信息展示的空間，在后續(xù)的開發(fā)中將實現(xiàn)模型的可視化顯示。通過交互式地運行系統(tǒng)，并將各進程的自動機圖形當前所處的位置和轉(zhuǎn)換標紅，更直觀形象地描述實時系統(tǒng)可能的動態(tài)行為及多并發(fā)進程之間的交互，從而開發(fā)出一個更加穩(wěn)定且高效的實時系統(tǒng)建模與驗證系統(tǒng)。