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