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