??? 摘 要：容錯和控制系統(tǒng)的安全性驗證是自發(fā)機撲系統(tǒng)成功的關(guān)鍵，一種叫做任務(wù)數(shù)據(jù)系統(tǒng)MDS (Mission Data Symstem)的控制框架的軟件理論被提了出來，而它的產(chǎn)生則推動了一種基于對象的控制方法的產(chǎn)生。本文將討論一種設(shè)計方法，該方法的設(shè)計目的是將對象網(wǎng)絡(luò)控制程序轉(zhuǎn)化為線性混合系統(tǒng)。該線性混合系統(tǒng)在使用信號模擬檢測器進行檢測時，在出現(xiàn)錯誤時是可以證明其安全性的。本文將結(jié)合例子介紹這種方法。
??? 關(guān)鍵詞：安全性驗證；機撲系統(tǒng)；MDS；模式檢測器
?
??? 天然形成的自發(fā)機撲系統(tǒng)有著復(fù)雜的控制系統(tǒng)?？偟膩碚f，為這些系統(tǒng)設(shè)置的錯誤提供必要的檢測、隔離、恢復(fù)軟件是復(fù)雜的，同時在模擬時會遇到一些出錯。在自發(fā)機撲系統(tǒng)中，需要一種系統(tǒng)地包含容錯功能的方法。一種實現(xiàn)的方式是產(chǎn)生一種當(dāng)出現(xiàn)錯誤時能夠自行重新配置的可變的控制系統(tǒng)。不過，假如該控制系統(tǒng)不能被證明是安全的，那么重新配置所產(chǎn)生的附加復(fù)雜性可能降低系統(tǒng)容錯能力的有效性。
??? 對模擬信號容錯控制系統(tǒng)來說，一種特別有用的方法是混合系統(tǒng)。關(guān)于混合系統(tǒng)的控制業(yè)界已經(jīng)付出了很多的努力，當(dāng)系統(tǒng)的聯(lián)系動力已經(jīng)是足夠簡單時，就可以驗證混合系統(tǒng)的運行不會進入不安全的狀態(tài)。有些軟件可以用于分析，包括HyTech、UPPAAL和VERITI。這都是信號模擬檢測器。本文所使用的檢測器是HyTech中一種叫做PHAVer的檢測器。通常為容錯混合控制系統(tǒng)所做的安全驗證，確保了當(dāng)一定的錯誤產(chǎn)生時,不會使系統(tǒng)進入一種不安全的狀態(tài)。控制系統(tǒng)必須通過一些合適的方式轉(zhuǎn)化為一種可接受的形式。一種這樣的工具是為了智能代理的轉(zhuǎn)化而產(chǎn)生，是叫做AgentSpeak的指向目標(biāo)的控制語言，其包含兩種模式轉(zhuǎn)化器。另一種流行的方式是從Buchi自動機對無限的字符使用設(shè)計控制程序進行更正。
??? 本文控制程序的軟件控制框架是基于任務(wù)數(shù)據(jù)系統(tǒng)(MDS)開發(fā)的。而MDS又是基于叫做狀態(tài)分析器的系統(tǒng)工程概念產(chǎn)生的。MDS能夠在連續(xù)衍生狀態(tài)中嚴格地認定有著分段恒定幅度的線性混合系統(tǒng)，同時能夠任意地處理大量的數(shù)據(jù)。使用MDS的系統(tǒng)被對象網(wǎng)絡(luò)所控制，該對象網(wǎng)絡(luò)在超時的時候直接對物理狀態(tài)表示約束的目的。本文將討論一個由對象網(wǎng)絡(luò)向線性混合系統(tǒng)自動轉(zhuǎn)化的過程。
1 背景信息
1.1 狀態(tài)分析和任務(wù)數(shù)據(jù)系統(tǒng)(MDS)
??? 狀態(tài)分析是一種引擎方法論，該方法論的設(shè)計集中于一種基于當(dāng)前狀態(tài)的系統(tǒng)設(shè)計方法。被控制系統(tǒng)中狀態(tài)效果的模式被用于狀態(tài)變量、系統(tǒng)控制、計劃和目的日程的評估。狀態(tài)變量是系統(tǒng)狀態(tài)或被控制或處于控制狀態(tài)屬性的代稱。狀態(tài)變量的例子可能包括機器人的位置坐標(biāo)、環(huán)境的溫度、感應(yīng)器的穩(wěn)定性、轉(zhuǎn)換器的位置。
??? 對象和對象描述產(chǎn)生于模式。對象處于一種目的的特殊語句中，該目的用來控制約束狀態(tài)變量的系統(tǒng)?；趯ο箢愋汀⒁?guī)則、目的的父對象可以詳細描述子對象。狀態(tài)分析的核心概念在于被用于設(shè)計控制系統(tǒng)的語言應(yīng)該與使用該控制系統(tǒng)的語言一致。因此，這種MDS軟件構(gòu)架應(yīng)該與狀態(tài)分析緊密相關(guān)。
??? 一個叫做軟件狀態(tài)變量的數(shù)據(jù)結(jié)構(gòu)是MDS的中心。一個狀態(tài)變量可以控制許多信息。例如，在飛機自動機中的位置狀態(tài)變量可以控制自動機的位置坐標(biāo)(x，y)、組件形式中的速度、每條信息中的不確認值。每個狀態(tài)變量的速度，但是卻會使位置和不確定值無法得到控制。
??? 對象網(wǎng)絡(luò)代替命令串成為系統(tǒng)的控制輸入。一個對象網(wǎng)絡(luò)由含有互相聯(lián)系的開始結(jié)束時間點的對象和暫存約束組成。一個對象的暫存約束可能基于執(zhí)行時間或者對象的完整性。對象可以引發(fā)由同樣性質(zhì)的或者其他偶然相關(guān)的狀態(tài)變量所描述的約束的產(chǎn)生。在對象網(wǎng)絡(luò)或?qū)ο蟮亩x中，對象通過對象調(diào)度軟件來進行調(diào)度，保證運行時沒有沖突發(fā)生。然后每個被調(diào)度的對象將被寄存器或狀態(tài)變量控制器所接收。
??? 定義表使MDS比基于命令行的控制體系能更靈活處理事物。一個例子如容錯，如果系統(tǒng)中存在物理冗余性，對錯誤對象的重定義有許多的處理方式。比如：有許多方式同樣能夠完成這項工作，或者為這項工作降低操作模式強度，對象的定義類可能會包含許多預(yù)定義策略。這些策略能通過不同的方式完成對象目的；而且它們可能被基于語法定義邏輯條件的描述器所選擇。這些能力使許多普通錯誤類型能自動地被控制系統(tǒng)所包容。
1.2 線性混合自動機
??? 有一些可用的抽象模式檢測器能夠驗證線性混合自動機。一個線性自動機由下面的組件組成：(1) 一個完整有序并包含連續(xù)狀態(tài)變量的表，x={X1, X2,…Xn}及它們相對應(yīng)的導(dǎo)出表y={Y1, Y2, …Yn}。(2) 一個有向圖(V, E)，V是系統(tǒng)控制模式或存儲空間的集合，E是在不同系統(tǒng)模式之間控制邊的集合。(3) 每個存儲空間的非變量集合inv(v)，初始條件集合init(v)，以及可變條件集合。在這些集合中v∈V。(4) 連接符號∑和連接操作A的集合。(5) 同步符號S的集合。以上組件完整地描述了一個可以使用PHAVer檢測器成功驗證的線性混合系統(tǒng)。在該混合自動機的安全驗證中使用的可達性分析法可以得出在一個有效回合里所以連接到一個確定狀態(tài)的所有狀態(tài)的集合。這可能引起該狀態(tài)空間巨大的溢出。PHAVer可以通過兩種方法處理該問題：(1) 通過把存儲空間分為簡單部分。(2) 使用存儲空間集合的過度近似值來限制系統(tǒng)的復(fù)雜性及加速聚合并促使過程停止。在分析中過度近似值并沒有要求，因為安全存在著嚴格的保證。
1.3 對象網(wǎng)絡(luò)轉(zhuǎn)換和驗證過程
??? 混合系統(tǒng)分析工具可以被用來驗證一個混合系統(tǒng)的安全行為，因此，對對象網(wǎng)絡(luò)驗證來說，一個由對象網(wǎng)絡(luò)向混合系統(tǒng)轉(zhuǎn)化的過程是對象網(wǎng)絡(luò)驗證的重要工具。轉(zhuǎn)化對象網(wǎng)絡(luò)的人工操作過程在圖1的轉(zhuǎn)換圖中可以表示出來。這些對象網(wǎng)絡(luò)由一些狀態(tài)變量和對象描述層，不過時間點必須加以嚴格控制，這意味著時間點在命令處于描述區(qū)的表中時開始計時。
?
??? 對象網(wǎng)絡(luò)中每一個狀態(tài)變量可被定義為可控制的、不可控制的或獨立的。一個可控狀態(tài)變量（簡稱CSV）直接地與一個命令類連接起來；一個不可控狀態(tài)變量(簡稱USV)無論如何都不與一個命令類發(fā)生聯(lián)系；一個獨立狀態(tài)變量(簡稱DSV)至少在一個可控狀態(tài)變量處有模塊獨立性。不同的混合自動元產(chǎn)生于這些不同狀態(tài)變量的對象。
??? 一個關(guān)于CSVs和DSVs的對象轉(zhuǎn)化過程的概述要點如下：
??? (1)在CSV和連續(xù)DSV上，分別為每個描述約束的對象建立描述和轉(zhuǎn)換邏輯表。
??? (2)向組中的連續(xù)點之間放置對象。
??? (3)在每個組中，通過連續(xù)葉對象和所有的父對象和約束CSVs的兄弟對象的方式產(chǎn)生存儲空間（模式）。為所有CSVs和約束在存儲單位中連續(xù)的DSVs設(shè)置標(biāo)簽，標(biāo)簽包括每一個有著動態(tài)更新方程的存儲空間。
??? (4)使用以上的描述和過度邏輯表在存儲單位和組之間產(chǎn)生以下轉(zhuǎn)換：①面向組的描述邏輯控制的轉(zhuǎn)換。②組內(nèi)存儲單位間錯誤的轉(zhuǎn)換。③邏輯轉(zhuǎn)換控制一個組向下個組或者下個存儲空間的轉(zhuǎn)換。
??? (5)增加基于時間的出口和失敗轉(zhuǎn)換，轉(zhuǎn)換為包含時間約束對象的存儲空間。當(dāng)轉(zhuǎn)換為連接組接口的存儲空間時，增加入口行為即重置時間變量為零。
??? (6)移除不必要的位置、組和轉(zhuǎn)化。
??? 對每個USV來說，一個獨立的混合自動機的形式源于來自于離散狀態(tài)或離散變量狀態(tài)集合的存儲空間的產(chǎn)生。轉(zhuǎn)換條件是或然率或基于狀態(tài)模式。對安全驗證來說，混合自動機被轉(zhuǎn)化為PHAVer代碼而且合適的轉(zhuǎn)化在自動機之間同步。不安全的集合被確認而且條件將使混合自動機進入不安全集合，這樣使用驗證軟件的條件就符合了。假如沒有這樣的條件符合，那么對象網(wǎng)絡(luò)就得以驗證。
2 轉(zhuǎn)換軟件設(shè)計
??? 對象網(wǎng)絡(luò)轉(zhuǎn)化過程的軟件版本不象早先提出的軟件版本那么復(fù)雜。但是大部分的重要能力都已經(jīng)包括在內(nèi)了。為了適應(yīng)表結(jié)構(gòu)顯示與它的相應(yīng)模式功能庫的要求，該軟件是以數(shù)學(xué)方式寫的。
2.1 軟件的輸入
??? 轉(zhuǎn)化軟件的輸入產(chǎn)生于一個可用對象網(wǎng)絡(luò)的必要設(shè)計組件。5個條件表(goals、usv、merge、elab、trans)是初始條件。在對象網(wǎng)絡(luò)中，對象表是一個關(guān)于所有可控制和獨立狀態(tài)變量的表。這些對象由父對象控制，沒有任何對象可以先于父對象出現(xiàn)。對象描述是一個由上到下的過程，因而對對象控制的約束是應(yīng)該獲得的基本條件。每一個對象入口都必須包含如下信息：
??? (1)對象數(shù)。這是為父約束設(shè)定的。
??? (2)時間表{Ts,Te}。該子表有兩個元素，開始時間點數(shù)和結(jié)束時間點數(shù)。這兩個時間點在指令控制下進行計數(shù)，且Ts=Te總為真。
??? (3)父對象數(shù)。假如對象沒有祖先時總為0。
??? (4)策略數(shù)。假如對象沒有父對象時為0。
??? (5)約束表{Sv,type,{C1,…Cn}}。該子表的第一個元素是獨立可控制的狀態(tài)變量數(shù)字字符（可控制的狀態(tài)變量集是強制定義的），即C1～Cn都是type制定類型的。狀態(tài)變量約束類型的數(shù)目，定義的約束類型在對象網(wǎng)絡(luò)中定義的所有不可控制變量組成了USV表。這些不可控制狀態(tài)表的命令都是強制型的。
??? 每一個USV入口必須有如下信息:
??? (1)狀態(tài)變量名。在所有描述和錯誤邏輯中使用的符號。這些符號對每一個不可控制狀態(tài)變量是獨一無二的。
??? (2)離散數(shù)值表{V1,…Vm}。該子表包含m離散數(shù)值或者未被控制的狀態(tài)變量數(shù)值集合。m的數(shù)值可以是數(shù)字或者是字符串，對特定的USV是唯一的，但不是對所有的USV都是唯一的。
??? (3)轉(zhuǎn)換表。{{{c,Vi},…},…,{{c,Vj},…}}。該表有m子表，每一個USV都含有一個離散數(shù)值。每一個子表中，都含有可以從狀態(tài)值中引出的轉(zhuǎn)換所組成的集合表。這些表中的第一個元素指轉(zhuǎn)換條件，第二個元素指轉(zhuǎn)換的結(jié)果。
??? 融合表有一些子表，在數(shù)字命令中每一個子表都包含一個可控制和相關(guān)狀態(tài)變量。這些子表包含了兩部分：
??? (1)描述可被代替的對象約束類型。
??? (2)假如兩個或更多同種狀態(tài)變量的約束同時活躍的話，這些約束類型是如何相互融合的。在這些子表中，還有一些關(guān)于自身融合和與比該約束數(shù)值大的約束融合的約束表。
??? 這部分的表包括以下內(nèi)容：
??? (1)融合類型。假如在約束中融合是有條件的，該值為-1。假如融合是不可能發(fā)生的，值為0，而且此時沒有更多的表元素。假如融合始終可能，該值為融合約束類型的數(shù)值。
??? (2)融合約束規(guī)則。這是指融合過程中，被實際約束值替代的和抽象化的規(guī)則。這可能是融合時最后入口。
??? (3)融合類型。僅僅對條件融合來說，約束類型的數(shù)目就是融合產(chǎn)生的結(jié)果。
??? 在目的表中，描述表為每個對象設(shè)立了一個子表。假如對象為父對象時，每個子表為不同的邏輯類型和條件單獨列表；若不是，為目的建立的子表就為空。這些詳細描述邏輯信息類型列表如下：
??? (1)“開始”邏輯。這種策略包括產(chǎn)生優(yōu)勢策略的詳盡描述的各種條件。
??? (2)“失敗”邏輯。這種策略表包括策略失敗和為了某種對象設(shè)定的策略失敗的條件。這時可能每一個策略不止一個條件，集和對象。該策略可能無法轉(zhuǎn)向安全狀態(tài)。同時，一個失敗的條件可能是標(biāo)有的“CGE”子對象的失敗的原因。
??? 每一個包含可控制和獨立的狀態(tài)變量的轉(zhuǎn)化表都有一個子表，子表中的表所以的條件在每一個含有可控制或獨立的狀態(tài)變量的約束類型中心必須為真，這些條件包含如下兩部分：
??? (1)輸入轉(zhuǎn)換邏輯。這個條件在輸入約束類型的時候必須為真。
??? (2)輸出轉(zhuǎn)換邏輯。這個條件表明了一種約束類型的完整性。
2.2 軟件輸出
??? 自從所有的USV自動機必要信息（除流以外）被輸入到軟件中，軟件就只有關(guān)于CSV/DSV目的自動機的信息了。這種叫做cdsva的結(jié)構(gòu)包括許多部分，開始被編入組然后編入?yún)^(qū)。在每個區(qū)表中，可以依次列出下列信息。
??? (1)已存在的對象表。表中內(nèi)容為對象數(shù)據(jù)。
??? (2)融合約束表。包括CSV和DSV數(shù)據(jù)，融合約束類型和約束值。
??? (3)開始轉(zhuǎn)化條件。只有當(dāng)條件已知時，轉(zhuǎn)化來自已存在組和當(dāng)前組之間的組連接器。
??? 輸入和輸出的轉(zhuǎn)化條件---這些轉(zhuǎn)化是從已存在的組連接器向存儲空間的轉(zhuǎn)化以及從存儲空間分別向后繼組連接器的轉(zhuǎn)化。條件則包括被約束于該空間的CSVs和DSVs。
??? (4)輸出錯誤轉(zhuǎn)換。包括列出的條件和可接受存儲空間?？赡苊總€位置不只一個輸出。
??? (5)輸出錯誤條件。條件和初始存儲空間都已列出?？赡苊總€空間不只一個輸出。
2.3 轉(zhuǎn)換算法
??? 在圖2中顯示了轉(zhuǎn)換軟件總的流程圖。在該圖中，轉(zhuǎn)換算法包括4個主要部分：存儲單元的產(chǎn)生、約束融合、轉(zhuǎn)換的產(chǎn)生和存儲單元的釋放。以下對這4個部分進行分別描述。
?
?
??? 存儲單元產(chǎn)生算法將對象輸入結(jié)構(gòu)，同時使用時間點、父對象和策略信息將對象分配進不同的組，然后分配進不同的存儲單元。由時間點信息首先開始這個過程。假如Te>Ts+1時，一些對象可以在不止一個組中產(chǎn)生。然后，父信息和策略信息將被用來在這個組中對每個對象查找它們所有的不相容對象。在不同的策略中，這些不相容對象不能像對象一樣在同樣的存儲單元中產(chǎn)生，是由于它們或者是寫入同樣的父對象，或者是來自同樣的父對象的對象所遺傳。然后，每一組分支對象都被找到而且都在存儲單元中產(chǎn)生；兄弟分支對象也合并入該位置。分支對象在這個組中沒有孩子，兄弟對象是寫入相同策略的對象或是在該組中沒有祖先的根對象（即與兄弟對象沒有共同的祖先），雙親對象和它們的兄弟在根對象到達時才被添加到每個存儲單元。每個存儲單元被其他可相容的單元聯(lián)合。當(dāng)沒有更多的單元可供融合時，多余的位置就被移除?？扇诤系奈恢靡话愎蚕淼礁嗟奈恢?，而且沒有一個存儲單元的對象是在其他單元的對象的不可相容對象表中的。這些步驟確保了每一個在兩個時間點之間的對象網(wǎng)絡(luò)執(zhí)行過程能夠明確地在一個位置被代表。
??? 約束融合算法使用寄存單元產(chǎn)生算法，對象和約束融合輸入將在每個存儲空間中所有的可控和獨立的狀態(tài)變量合并產(chǎn)生約束。對同一狀態(tài)變量的約束對象類型進行對比可以發(fā)現(xiàn)融合輸入的合適區(qū)域。然后符號的融合條件和融合約束值被對象輸入中的實際約束所代替。如果融合是成功的，新的融合類型和融合約束被增加到該存儲空間。如果融合不成功，該空間將被釋放。
??? 轉(zhuǎn)換產(chǎn)生算法產(chǎn)生三種轉(zhuǎn)換：(1)由之前接入每個組的存儲空間的組連接器的轉(zhuǎn)換；(2)在一個組中存儲空間之間的失敗轉(zhuǎn)換；(3)從一個存儲空間向下一個組連接器的轉(zhuǎn)換（該連接器使用對象、elab、trans、usv和融合約束算法輸出部分作為輸入）。在每個存儲單元中，某一對象的“開始”邏輯通過“與”運算簡化后檢查是否為真。如果邏輯結(jié)果表達式為假，那么該轉(zhuǎn)換被拋棄。存儲空間中基于結(jié)束類型的所有的約束狀態(tài)變量的轉(zhuǎn)換邏輯也是經(jīng)過運算并簡化。在每個存儲單元中，每個對象的錯誤邏輯將會被列舉出來，同時在同一存儲空間中的失敗轉(zhuǎn)化也會通過“或”運算進行運算并簡化。將要接受失敗轉(zhuǎn)化的存儲空間將被更新并反映這一事實。一個未被簡化的cdsva結(jié)構(gòu)是這一算法部分的輸出。
??? 存儲單元釋放算法檢查一些保證存儲單元或每一個存儲單元組的釋放的條件，并在條件為真時釋放存儲單元，這些條件包括：(1)輸入條件的缺失；(2)一個總為真的失敗條件；(3)存儲空間的釋放包括所有其他原因該存儲空間及替代被刪除空間的重新賦值的新存儲空間的錯誤條件的釋放；(4)出口條件是所有的輸入轉(zhuǎn)化條件的子集。算法的輸出cdsva表是軟件的最終輸出。
3 舉例
??? 一個已知的正方形房子被分為4個區(qū)域（如圖3），一個機器人在該房子中尋找目標(biāo)，它可能在或區(qū)中，假如機器人在某區(qū)中找到了，那么它就將停在那里;否則它將繼續(xù)尋找。被用來解決該問題的一段對象網(wǎng)絡(luò)和混合自動機軟件結(jié)構(gòu)如圖4所示。該軟件的輸入由10個對象，一個可控狀態(tài)變量，包含兩個約束類型（驅(qū)動和停留）的坐標(biāo)，一個不可控狀態(tài)變量，目標(biāo)的存儲空間。該空間包含3個離散狀態(tài)（P2,P4,或不存在），以及含有描述邏輯的4個父對象。
?
?
?
??? 當(dāng)目標(biāo)不存在或者機器人離開P2或P4區(qū)找到目標(biāo)時，按照本算法設(shè)計的混合自動機在運行時會被PHAVer檢測到處于一個不安全或者不正確的集合中。模式檢測器就找不出使機器人進入不安全狀態(tài)的混合自動機的不安全執(zhí)行進程了。這個問題的解決辦法可以簡便地通過該對象網(wǎng)絡(luò)轉(zhuǎn)換和驗證過程得以發(fā)現(xiàn)并驗證。
??? 本文所給的對象網(wǎng)絡(luò)轉(zhuǎn)換軟件能夠快速與精確地將復(fù)雜的對象網(wǎng)絡(luò)轉(zhuǎn)化為線性混合自動機。該自動機可以通過現(xiàn)在的符號模式檢測軟件如PHAVer得到驗證。該自動工具能使更多的對象網(wǎng)絡(luò)得以驗證，因而對于基于對象控制程序特別是如MDS的控制構(gòu)架有特別的促進作用。
參考文獻
[1]?張達科,胡躍明.一類仿射非線性混合系統(tǒng)的去混合化控制[J]. 華南理工大學(xué)學(xué)報, 2004，32(11): 32-35.
[2]?董威,王戟,齊治昌. 并發(fā)和實時系統(tǒng)的模型檢驗技術(shù)[J]. 計算機研究與發(fā)展，2001，06: 24-27.
[3]?康宇,奚宏生,季海波，等. 一類不確定混合線性系統(tǒng)魯棒自適應(yīng)控制[N].中國科學(xué)技術(shù)大學(xué)學(xué)報，2004(6): 45-48.
[4]?吳為民.數(shù)字系統(tǒng)的形式化驗證[N]. 計算機世界報，2005，37:11-12.
[5]?王巧麗.SPIN模型檢測的研究與應(yīng)用[J]. 貴州大學(xué)學(xué)報,2006，10：17-20.
[6]?Holzmann, Gerard .The SPIN Model Checker, Pearson.
[7]?Labinaz G,Bayoumi M.M, Rudie K.A survey of modeling and control of hybrid systems. Annual Reviews of Control,1997.
[8]?Henzinger T, Ho P.-H, Toi H W. HyTech:A model checker for hybrid systems. International Journal on software Tools for Technology Transfer, 1997.
[9]?Henzinger T, Ho P. -H. Automatic symbolic verification of embedded systems.IEEE Transactions on Software Engineering,1996, 22 (3). 181-201.
[10]?Dvorak D,Rasmussen R, Starbrid T. State knowledge representation in the Mission Data System. IEEE Aerospace Conference, 2002.