嵌入式控制系統(tǒng)時(shí)序安全性建模及驗(yàn)證

范寶文，包 健

(1.杭州電子科技大學(xué)網(wǎng)絡(luò)空間安全學(xué)院，浙江 杭州 310018；2.杭州電子科技大學(xué)計(jì)算機(jī)學(xué)院，浙江 杭州 310018)

0 引 言

嵌入式控制系統(tǒng)在工業(yè)領(lǐng)域的應(yīng)用愈發(fā)普遍，如何保證控制系統(tǒng)時(shí)序邏輯的正確性一直是學(xué)術(shù)界和工業(yè)界研究的熱點(diǎn)。傳統(tǒng)測(cè)試方法的效果往往取決于測(cè)試用例的規(guī)模，很難保證程序運(yùn)行時(shí)的邏輯符合系統(tǒng)設(shè)計(jì)[1]。此外，C語(yǔ)言編寫的嵌入式控制系統(tǒng)引入了時(shí)間相關(guān)的模塊和控制邏輯，和普通的C語(yǔ)言程序有較大不同，增大了測(cè)試難度。形式化方法是對(duì)系統(tǒng)安全性進(jìn)行驗(yàn)證的有效工具，主要分為模型檢測(cè)和定理證明。模型檢測(cè)方法運(yùn)用驗(yàn)證工具窮舉系統(tǒng)的狀態(tài)空間，較好地利用驗(yàn)證工具來(lái)驗(yàn)證有窮程序，如借助Uppaal和時(shí)間自動(dòng)機(jī)[2-4]對(duì)可編程邏輯控制器(Programmable Logic Controller，PLC)程序建模，或使用SMV[5-6]來(lái)驗(yàn)證PLC程序的時(shí)序性質(zhì)，但該方法不適用于帶有時(shí)間模塊的C語(yǔ)言程序等復(fù)雜遞歸的情況，容易出現(xiàn)狀態(tài)空間爆炸問(wèn)題。定理證明方法基于霍爾邏輯等形式邏輯系統(tǒng)對(duì)系統(tǒng)狀態(tài)進(jìn)行推理，借助交互式證明助手進(jìn)行證明：基于Coq的研究[7-9]對(duì)PLC程序語(yǔ)義進(jìn)行探討，但僅采用一階謂詞等低層次的規(guī)約公式來(lái)描述系統(tǒng)約束，不利于方法的推廣；Gerwin等[10]使用Isabell[11]對(duì)C語(yǔ)言的程序進(jìn)行驗(yàn)證，但忽略了時(shí)序性質(zhì)的形式化描述與建模，使得模型在時(shí)序性質(zhì)表達(dá)能力上有所欠缺。本文采用定理證明方法，提出一種基于Coq的嵌入式控制建模和系統(tǒng)時(shí)序性質(zhì)驗(yàn)證方法，采用線性時(shí)序邏輯(Linear Temporal Logic，LTL)描述安全性質(zhì)，建立控制系統(tǒng)和LTL公式的形式化模型，有效驗(yàn)證了系統(tǒng)是否符合提出的時(shí)序安全約束。

1 中間模型建模方法

由于直接采用驗(yàn)證工具來(lái)描述系統(tǒng)有較大的難度，所以通過(guò)中間模型建模的方法應(yīng)用廣泛[12]。本文選取有限自動(dòng)機(jī)作為實(shí)現(xiàn)中間模型的工具，將系統(tǒng)的運(yùn)行描述為自動(dòng)機(jī)的狀態(tài)轉(zhuǎn)移，制定轉(zhuǎn)移的語(yǔ)義公式，并將得到的自動(dòng)機(jī)中間模型作為形式化建模方法的輸入。

本文的實(shí)驗(yàn)對(duì)象是1個(gè)C語(yǔ)言編寫的3軸直角坐標(biāo)機(jī)器人控制系統(tǒng)，機(jī)器人示意圖如圖1所示。機(jī)械臂可以在2個(gè)水平方向和1個(gè)豎直方向上移動(dòng)，分別用X，Y，Z表示。此外有1個(gè)帶有受控機(jī)械手的球桶釋放小球，使得小球可以在Z軸方向自由下落。

圖1 直角坐標(biāo)機(jī)器人示意圖

1.1 控制系統(tǒng)到自動(dòng)機(jī)的建模

建模路線與思路如圖2所示，主要分為6個(gè)步驟：前4個(gè)步驟分別定義自動(dòng)機(jī)相關(guān)的數(shù)據(jù)類型；第5步以推導(dǎo)公式的形式建立自動(dòng)機(jī)的語(yǔ)義模型，規(guī)范其轉(zhuǎn)移規(guī)則；第6步在保持語(yǔ)義不變的情況下優(yōu)化自動(dòng)機(jī)模型，使其更貼近原系統(tǒng)。

圖2 基于自動(dòng)機(jī)的系統(tǒng)建模過(guò)程示意圖

(1)定義系統(tǒng)的變量空間。定義系統(tǒng)的變量空間State是當(dāng)前自動(dòng)機(jī)模型中變量值的集合。為了區(qū)別普通的變量類型，將系統(tǒng)的變量空間稱為“系統(tǒng)的狀態(tài)”。系統(tǒng)的狀態(tài)是1個(gè)3元組(c,v,w)，分別表示當(dāng)前機(jī)械臂終端所在坐標(biāo)、寄存器的值和機(jī)械手的開(kāi)關(guān)狀態(tài)。

(2)定義系統(tǒng)運(yùn)行階段集合。系統(tǒng)運(yùn)行過(guò)程根據(jù)其特點(diǎn)被邏輯劃分為5個(gè)階段，用Mode={idle,static,ready,run,pending}表示。idle表示系統(tǒng)上電復(fù)位但未運(yùn)行；static表示系統(tǒng)完成初始化；ready表示運(yùn)動(dòng)的準(zhǔn)備工作已就緒；run表示系統(tǒng)發(fā)出脈沖信號(hào)后，電機(jī)驅(qū)動(dòng)皮帶開(kāi)始運(yùn)轉(zhuǎn)；pending表示機(jī)械臂末端根據(jù)計(jì)時(shí)器保持一定時(shí)間懸空的狀態(tài)。

(3)定義系統(tǒng)抽象指令集合。機(jī)器人控制系統(tǒng)的一系列行為均通過(guò)改變寄存器的值或全局變量的值來(lái)實(shí)現(xiàn)，可以抽象為“行為指令”的集合Instr={start,stop,calculate,move,delay,return,hold,release}，其作用在于改變系統(tǒng)內(nèi)部數(shù)值。行為指令集合可直接應(yīng)用于自動(dòng)機(jī)模型，作為其標(biāo)簽事件的集合。

(4)定義系統(tǒng)的格局與轉(zhuǎn)移關(guān)系。定義系統(tǒng)的格局Configuration是系統(tǒng)運(yùn)行某一時(shí)刻所有描述元素的數(shù)據(jù)結(jié)構(gòu)，是1個(gè)3元素的笛卡爾積。將時(shí)間離散化處理，1個(gè)格局可寫為(μ,τ,σ)，其中μ表示當(dāng)前系統(tǒng)所處的階段；τ是離散化全局時(shí)間變量，表示當(dāng)前時(shí)刻；σ表示τ系統(tǒng)的狀態(tài)。系統(tǒng)的轉(zhuǎn)移關(guān)系是1個(gè)3元組(C,f,C0)。其中C表示系統(tǒng)的格局，f表示遷移函數(shù)，C0表示系統(tǒng)的初始格局。

通過(guò)上述步驟，建立圖3(a)所示機(jī)器人控制系統(tǒng)自動(dòng)機(jī)，其中自動(dòng)機(jī)的狀態(tài)來(lái)自步驟2定義的系統(tǒng)運(yùn)行階段，自動(dòng)機(jī)的輸入來(lái)自步驟3定義的抽象行為指令。圖3(b)為機(jī)器人機(jī)械手的狀態(tài)轉(zhuǎn)移圖。idle為起始狀態(tài)，on和off分別表示機(jī)械手的開(kāi)合。

(5)建立自動(dòng)機(jī)轉(zhuǎn)移的語(yǔ)義模型。模型的語(yǔ)義標(biāo)注不僅能詳細(xì)描述模型內(nèi)部的細(xì)節(jié)，還能為不同層次模型的抽象、部件間的并發(fā)行為提供形式化的支持。以延時(shí)計(jì)時(shí)器指令delay為例，其對(duì)系統(tǒng)格局改變的語(yǔ)義公式如下：

(1)

(2)

橫線上的內(nèi)容描述了系統(tǒng)狀態(tài)的改變，A(i)標(biāo)記當(dāng)前要執(zhí)行的指令，橫線下的內(nèi)容描述系統(tǒng)格局的改變。式(1)表示，收到delay指令后，系統(tǒng)由“run”狀態(tài)進(jìn)入“pending”狀態(tài)，并啟動(dòng)計(jì)時(shí)器開(kāi)始計(jì)時(shí)，時(shí)間變量x開(kāi)始自增。式(2)表示，當(dāng)計(jì)時(shí)器時(shí)間變量x大于等于設(shè)定的時(shí)間參數(shù)y時(shí)，x清零，系統(tǒng)由“run”狀態(tài)進(jìn)入“static”狀態(tài)。

(6)組合自動(dòng)機(jī)。步驟4分別建立了機(jī)械臂和機(jī)械手的狀態(tài)轉(zhuǎn)移自動(dòng)機(jī)，但無(wú)法表現(xiàn)出機(jī)械臂移動(dòng)與機(jī)械手開(kāi)合的并發(fā)執(zhí)行關(guān)系。因此，采用平行同步組合的方法，將圖3(a)與圖3(b)中自動(dòng)機(jī)進(jìn)行組合，得到新的自動(dòng)機(jī)，更好地展示并發(fā)執(zhí)行的時(shí)序細(xì)節(jié)。新自動(dòng)機(jī)的狀態(tài)空間來(lái)自2個(gè)輸入自動(dòng)機(jī)狀態(tài)空間的交叉乘積，新的轉(zhuǎn)移關(guān)系來(lái)自原自動(dòng)機(jī)中轉(zhuǎn)移關(guān)系的交集，得到的結(jié)果如圖3(c)所示。

圖3 控制系統(tǒng)、機(jī)械手狀態(tài)轉(zhuǎn)移自動(dòng)機(jī)及組合結(jié)果

1.2 時(shí)序安全性約束

結(jié)合圖3(c)中的系統(tǒng)組合結(jié)果，提出直角坐標(biāo)機(jī)器人控制系統(tǒng)必須滿足的幾個(gè)時(shí)序約束，并對(duì)應(yīng)使用LTL公式描述為系統(tǒng)屬性。

屬性1當(dāng)機(jī)械手松開(kāi)小球后，狀態(tài)機(jī)立即進(jìn)入“pending,on”狀態(tài)。令φ1表示指令為機(jī)械手松開(kāi)時(shí)為true，φ2表示系統(tǒng)處于“pending”狀態(tài)為true，公式表述為G(φ1→Fφ2)。

屬性2在機(jī)械臂運(yùn)動(dòng)階段時(shí)，機(jī)械手應(yīng)保持“off”狀態(tài)，以保證系統(tǒng)的安全運(yùn)行。令φ3表示系統(tǒng)處于“run”狀態(tài)時(shí)為true，φ4表示機(jī)械手處于關(guān)閉狀態(tài)為true，公式表述為G(φ3∧φ4)。

2 在Coq中形式化建模與驗(yàn)證

第1節(jié)將控制系統(tǒng)的運(yùn)行用狀態(tài)轉(zhuǎn)移圖表示為自動(dòng)機(jī)中間模型，并使用LTL公式描述系統(tǒng)應(yīng)滿足的時(shí)序安全約束。本節(jié)在此基礎(chǔ)上建立系統(tǒng)在Coq中的模型，并驗(yàn)證時(shí)序結(jié)束是否成立。首先，基于自動(dòng)機(jī)語(yǔ)義，形成系統(tǒng)在Coq中的模型；然后，在Coq中建立LTL的模型，以便形式化地描述1.2節(jié)中提出的系統(tǒng)時(shí)序安全屬性；最后，將屬性表述為Coq中的定理，并選擇合適的策略證明。建模與驗(yàn)證的總體思路如圖4所示。

圖4 Coq中的建模與驗(yàn)證過(guò)程示意圖

2.1 Coq中系統(tǒng)模型的建立

通過(guò)數(shù)據(jù)類型映射的方法，逐步將描述系統(tǒng)運(yùn)行的自動(dòng)機(jī)轉(zhuǎn)換為Coq中的形式化模型，作為時(shí)序性質(zhì)驗(yàn)證的載體。

(1)形式化定義系統(tǒng)變量。定義基礎(chǔ)變量類型。全局時(shí)鐘、距離均為自增整數(shù)，使用Coq中的自然數(shù)類型nat定義，分別命名為為Distance和Time。為了簡(jiǎn)化建模過(guò)程，將機(jī)械手的狀態(tài)ClawState定義為布爾類型的變量，足以描述其特性。定義坐標(biāo)類型變量Coordinate為1個(gè)3元組。

使用Coq中的Inductive類型將1.1節(jié)步驟1定義的系統(tǒng)狀態(tài)描述為1個(gè)3元組。其中參數(shù)c表示機(jī)械臂末端當(dāng)前坐標(biāo)，v表示寄存器變量的集合，函數(shù)total_map表示字符串類型的編號(hào)到多態(tài)類型數(shù)值的映射關(guān)系。

(2)形式化定義系統(tǒng)運(yùn)行階段。對(duì)照1.1節(jié)中運(yùn)行階段的定義，使用枚舉的方法定義系統(tǒng)的運(yùn)行階段Mode，表示如下：

(3)形式化定義系統(tǒng)行為指令。行為指令在定義時(shí)分為2種類型S_Instr和M_Instr，分別使系統(tǒng)的狀態(tài)或系統(tǒng)的格局發(fā)生改變。S_Instr類型定義了更新系統(tǒng)狀態(tài)的指令，包括機(jī)械手開(kāi)合指令Release，Hold，寫內(nèi)存操作Write和坐標(biāo)更新操作Move_S。M_Instr類型定義了更新系統(tǒng)格局的指令。

(4)形式化定義系統(tǒng)格局與轉(zhuǎn)移關(guān)系。依據(jù)1.1節(jié)步驟4所定義的系統(tǒng)格局Configuration，使用Inductive類型將其描述為1個(gè)3元組，其中的3個(gè)元素分別表示系統(tǒng)運(yùn)行階段m、系統(tǒng)狀態(tài)v和全局時(shí)鐘變量t。

轉(zhuǎn)移關(guān)系定義為Coq中的函數(shù)，輸入?yún)?shù)分別為當(dāng)前系統(tǒng)格局Configuration(設(shè)為g)和當(dāng)前指令M_Instr(設(shè)為I)，輸出參數(shù)為新的系統(tǒng)格局。限于篇幅這里僅給出函數(shù)的定義。

2.2 Coq中LTL公式模型的建立

將LTL公式的語(yǔ)法和語(yǔ)義轉(zhuǎn)換為Coq中的形式化模型。1.2小節(jié)中提出的屬性可被描述為Coq中的定理，并嵌入2.1小節(jié)中建立的系統(tǒng)模型進(jìn)行驗(yàn)證。在Coq中建立LTL公式的形式化模型分為3步。首先，聲明LTL公式的語(yǔ)法，定義不同的函數(shù)運(yùn)算；然后，定義路徑的變量類型和輔助函數(shù)；最后，結(jié)合語(yǔ)法和路徑類型變量定義LTL公式的語(yǔ)義函數(shù)。

(1)形式化定義LTL語(yǔ)法。類型LTL_Formula定義了線性時(shí)序邏輯公式的語(yǔ)法。AP表示原子命題的類型。Statement和Neg_Statement定義了基于原子命題的LTL公式，分別表示其肯定和否定的形式。Conj，Disy和Imply是作用于2個(gè)LTL公式的謂詞，分別定義了語(yǔ)法中合取、析取和蘊(yùn)含這3種邏輯連接符。這3個(gè)函數(shù)接受2個(gè)LTL公式作為參數(shù)，返回1個(gè)新的LTL公式。Until表示基礎(chǔ)時(shí)序算子“U”，Release是Until運(yùn)算符的擴(kuò)展，這2個(gè)函數(shù)接受2個(gè)LTL公式作為參數(shù)，返回1個(gè)新的LTL公式。Next表示基礎(chǔ)時(shí)序算子“X”，接受1個(gè)LTL公式作為參數(shù)，返回1個(gè)新的LTL公式。

(*LTL語(yǔ)法定義*)

|Statement∶AP→LTL_Formula|Neg_Statement∶AP→LTL_Formula

|Conj∶LTL_Formula→LTL_Formula→LTL_Formula|Disy∶LTL_Formula→LTL_Formula→LTL_Formula|Imply∶LTL_Formula→LTL_Formula→LTL_Formula

|Until∶LTL_Formula→LTL_Formula→LTL_Formula|Release∶LTL_Formula→LTL_Formula→LTL_Formula|Next∶LTL_Formula→LTL_Formula.

(2)形式化定義LTL路徑變量類型。LTL中的“路徑”可以看作1個(gè)無(wú)限長(zhǎng)度的狀態(tài)序列，路徑類型Path是原子命題類型到布爾值的映射。Index_Path函數(shù)獲取1條路徑和1個(gè)狀態(tài)作為參數(shù)，返回1條路徑中該狀態(tài)的布爾值。Sub_Path函數(shù)同樣需要1條路徑和1個(gè)狀態(tài)作為傳入?yún)?shù)，不同之處在于使用了匿名函數(shù)機(jī)制，函數(shù)返回類型變成了路徑。

(3)形式化定義LTL語(yǔ)義。借助Coq中Fixpoint類型遞歸地定義LTL公式語(yǔ)義函數(shù)，包括路徑類型變量σ和LTL公式類型變量φ兩個(gè)參數(shù)。函數(shù)使用match結(jié)構(gòu)分情況討論參數(shù)φ，類似于C語(yǔ)言中的case結(jié)構(gòu)，共有8種可能性，分別為：

① |Statementa?(Index_Pathσ0)a=true

② |Neg_Statementa?(Index_Pathσ0)a=false

③ |Conjφ1φ2?(LTL_Semanticsσφ1)∧(LTL_Semanticsσφ2)

④ |Disyφ1φ2?(LTL_Semanticsσφ1) ∨ (LTL_Semanticsσφ2)

⑤ |Implyφ1φ2?(LTL_Semanticsσφ1) → (LTL_Semanticsσφ2)

⑥ |Untilφ1φ2?existsi,LTL_Semantics(Sub_Pathσi)φ2∧ (forallj,jLTL_Semantics(Sub_Pathσj)φ1)

⑦|Releaseφ1φ2?(foralli,LTL_Semantics(Sub_Pathσi)φ2) ∨existsi, (LTL_Semantics(Sub_Pathσi)φ2) ∧(forallj,j?i→LTL_Semantics(Sub_Pathσj)φ1)

⑧ |Nextφ1?LTL_Semantics(Sub_Pathσ1)φ1end.

LTL的語(yǔ)義函數(shù)按功能的不同可歸納為4種情況，具體的說(shuō)明如下：

(1)分支1、分支2：“Statement a”表示1個(gè)真值為true的原子命題類型的公式，其中a是AP類型變量。該公式和“Neg_Statement a”是遞歸邊界，表示該命題對(duì)路徑起始狀態(tài)是否成立。

(2)分支3、分支4、分支5：描述了邏輯連接符對(duì)LTL公式的作用。合取公式“Conjφ1φ2”表明若φ1，φ2都對(duì)路徑σ成立，則φ1，φ2的合取對(duì)路徑σ成立；析取公式“Disyφ1φ2”表示若φ1,φ2中的1個(gè)對(duì)路徑σ成立，則φ1，φ2的析取對(duì)路徑σ成立；蘊(yùn)含公式“Implyφ1φ2”表示若φ1對(duì)路徑σ成立，則推出φ2對(duì)路徑σ也成立。

(3)分支6、分支7：描述了時(shí)態(tài)算子的語(yǔ)義?！癠ntilφ1φ2”表示存在狀態(tài)i>=0，使得所有的0?j?i，有φ2在后綴qj,qj+1,qj+2,...中成立，且φ1在后綴qi,qi+1,qi+2,...中成立；“Releaseφ1φ2”表明，若φ1可以一直成立，則該式對(duì)路徑上的所有狀態(tài)都成立；或存在狀態(tài)i>=0，存在1個(gè)狀態(tài)i>=0，使得所有的0?j?i，有φ2在后綴qj,qj+1,qj+2,...中成立，且φ1在后綴qi,qi+1,qi+2,...中成立。

(4)分支8：“Nextφ1”表明，若使“Nextφ1”對(duì)路徑σ={q0,q1,q2,q3,...}成立，當(dāng)且僅當(dāng)公式φ1對(duì)后綴{q1,q2,q3,...}上的所有狀態(tài)成立。

補(bǔ)充的時(shí)序算子G和F可根據(jù)時(shí)序算子U和V的定義擴(kuò)展而來(lái)，定義如下：

2.3 時(shí)序安全性質(zhì)的驗(yàn)證

以1.2小節(jié)中屬性2為例展示定義的證明步驟，將其所述性質(zhì)描述為定理Spec_2，如下所示。

①TheoremSpec_2∶forall(g∶Configuration)(σ∶Path),

② (eqb_mode(getModeg)run)g=true→

③σ//(G(Statement(ap((eqb_mode(getModeg)run)g))g)∧(Neg_Statement(ap(～(get_claw(getStateg))g))g)).

第1步使用Theorem 關(guān)鍵字定義定理，包括系統(tǒng)格局類型參數(shù)g和路徑類型參數(shù)σ。第2步描述了定理的假設(shè)，即當(dāng)前系統(tǒng)運(yùn)行于“run”階段，eqb_mode函數(shù)比較2個(gè)運(yùn)行階段是否相等，getMode用于獲取1個(gè)格局中的運(yùn)行階段。第3步陳述了定理的內(nèi)容，當(dāng)滿足第2步條件時(shí)，自動(dòng)機(jī)應(yīng)滿足公式“G (φ3∧ φ4)”。其中“φ3：Statement (ap (p3_1 g)) g”表示系統(tǒng)處于“run”狀態(tài)時(shí)為true，“φ4：Neg_Statement (ap (p3_2 g)) g”表示機(jī)械手處于關(guān)閉狀態(tài)為true。ap是1個(gè)原子命題AP類型的變量，用于將自動(dòng)機(jī)語(yǔ)法表示的命題轉(zhuǎn)換為線性時(shí)序邏輯中的原子命題類型公式。

定理Spec_2證明過(guò)程的主要思路如下：首先，依據(jù)LTL恒等式“G (φ3∧φ4)≡Gφ3∧Gφ4”，將定理的形式化簡(jiǎn)為2個(gè)子公式的合取。然后，使用split策略分解定理為2個(gè)子命題，證明目標(biāo)變?yōu)榉謩e證明路徑σ符合2個(gè)子公式。最后，分別使用關(guān)鍵字left和right進(jìn)入子命題的證明上下文，選取合適的策略證明目標(biāo)。后續(xù)證明的過(guò)程限于篇幅不再贅述。

屬性2和屬性3實(shí)現(xiàn)了完整的證明，表明控制系統(tǒng)滿足1.2小節(jié)中提出的對(duì)應(yīng)約束。屬性1在推導(dǎo)過(guò)程中發(fā)現(xiàn)了錯(cuò)誤：系統(tǒng)同時(shí)收到stop(外部開(kāi)關(guān)指令)和delay(內(nèi)部設(shè)定指令)這種極為少見(jiàn)的情況時(shí)，仍會(huì)進(jìn)入到包含“pending”的懸停狀態(tài)，如圖5所示。從狀態(tài)1出發(fā)，遇到stop指令時(shí)應(yīng)轉(zhuǎn)移到狀態(tài)2，但通過(guò)推導(dǎo)，自動(dòng)機(jī)錯(cuò)誤地通過(guò)虛線轉(zhuǎn)移到狀態(tài)3。通過(guò)與控制系統(tǒng)開(kāi)發(fā)工程師的交流驗(yàn)證了證明的結(jié)果，并修改了原系統(tǒng)，提高了外部開(kāi)關(guān)指令處理的優(yōu)先級(jí)，使得系統(tǒng)在收到外部開(kāi)關(guān)指令時(shí)會(huì)優(yōu)先處理，消除了1個(gè)隱藏的邏輯錯(cuò)誤，提高了系統(tǒng)的時(shí)序安全性。

圖5 錯(cuò)誤狀態(tài)轉(zhuǎn)移示意圖

3 結(jié)束語(yǔ)

本文針對(duì)C語(yǔ)言編程的嵌入式控制系統(tǒng)時(shí)序安全問(wèn)題，提出一種基于Coq的系統(tǒng)建模和時(shí)序性質(zhì)驗(yàn)證方法。通過(guò)分析1個(gè)機(jī)器人控制系統(tǒng)，發(fā)現(xiàn)了系統(tǒng)中傳統(tǒng)測(cè)試方法無(wú)法檢測(cè)出來(lái)的隱藏時(shí)序邏輯錯(cuò)誤，證明了本方法的有效性。本方法可以推廣到由C語(yǔ)言編寫的更為復(fù)雜的嵌入式控制系統(tǒng)程序的建模及驗(yàn)證工作上。下一步將建立更精確的定時(shí)器模型，在代碼層面對(duì)控制系統(tǒng)的函數(shù)及算法進(jìn)行建模，分析系統(tǒng)的異步時(shí)序行為。