鞠秀芳

(南京大學(xué)中國(guó)社會(huì)科學(xué)研究評(píng)價(jià)中心,江蘇南京210093)

0 引言

嵌入式系統(tǒng)是以應(yīng)用為中心，以解決特定任務(wù)為目的，致力于提高應(yīng)用系統(tǒng)功能、可靠性、成本、體積、功耗的專用計(jì)算機(jī)系統(tǒng)．嵌入式系統(tǒng)對(duì)時(shí)間的要求有嚴(yán)格的限制，系統(tǒng)在接到處理請(qǐng)求的同時(shí)，必須在規(guī)定的時(shí)間內(nèi)響應(yīng)并完成任務(wù)處理．實(shí)時(shí)性的保證不僅與系統(tǒng)的調(diào)度設(shè)計(jì)有關(guān)，還取決于實(shí)際運(yùn)行時(shí)系統(tǒng)對(duì)事件的具體調(diào)度處理和響應(yīng)時(shí)間等．中斷是嵌入式系統(tǒng)進(jìn)行實(shí)時(shí)響應(yīng)的重要機(jī)制，其觸發(fā)的不可預(yù)測(cè)性使得系統(tǒng)運(yùn)行時(shí)的時(shí)序較復(fù)雜．尤其是在允許中斷嵌套的多級(jí)中斷驅(qū)動(dòng)系統(tǒng)中，一次中斷請(qǐng)求在系統(tǒng)響應(yīng)過(guò)程中可能會(huì)多次被高優(yōu)先級(jí)的中斷掛起，這就給系統(tǒng)的時(shí)間約束保證帶來(lái)了困難．提供有效的中斷驅(qū)動(dòng)系統(tǒng)設(shè)計(jì)和驗(yàn)證方法可以在保證系統(tǒng)功能性需求的同時(shí)保證系統(tǒng)的時(shí)間約束，并為系統(tǒng)設(shè)計(jì)的正確性提供保障．

中斷驅(qū)動(dòng)系統(tǒng)中，任務(wù)的實(shí)際執(zhí)行軌跡是由任務(wù)的優(yōu)先級(jí)以及中斷源共同驅(qū)動(dòng)的．由于中斷觸發(fā)的不可預(yù)測(cè)性，且高優(yōu)先級(jí)中斷可以隨時(shí)打斷處理低優(yōu)先級(jí)中斷的任務(wù)，因此，系統(tǒng)可能的運(yùn)行軌跡組成的空間是無(wú)窮的．傳統(tǒng)的以測(cè)試為基礎(chǔ)的方法，無(wú)法完全遍歷整個(gè)運(yùn)行軌跡空間，其有效性有很大局限性．同時(shí)，為使得被測(cè)系統(tǒng)按照指定的軌跡運(yùn)行，需要搭建相應(yīng)的測(cè)試支撐環(huán)境，并設(shè)計(jì)有效的測(cè)試用例，測(cè)試的代價(jià)是相當(dāng)昂貴的．

當(dāng)前研究主要是通過(guò)自動(dòng)驗(yàn)證技術(shù)，構(gòu)造系統(tǒng)的行為模型，并運(yùn)用模型驗(yàn)證技術(shù)來(lái)驗(yàn)證系統(tǒng)的設(shè)計(jì)對(duì)滿足給定的時(shí)間約束性的有效性．已有的工作以時(shí)間自動(dòng)機(jī)[1?3]和Petri網(wǎng)[4]為建模工具，對(duì)應(yīng)用非搶占式調(diào)度策略系統(tǒng)的時(shí)間約束進(jìn)行驗(yàn)證．由于中斷驅(qū)動(dòng)系統(tǒng)的任務(wù)調(diào)度必須是搶占式的，而上述建模工具無(wú)法對(duì)系統(tǒng)的搶占式調(diào)度行為進(jìn)行建模，因而這些研究工作不能直接處理中斷驅(qū)動(dòng)系統(tǒng)．在[5]中，B′erard等研究者提出了中斷時(shí)間自動(dòng)機(jī)作為描述中斷驅(qū)動(dòng)系統(tǒng)的建模工具．中斷時(shí)間自動(dòng)機(jī)引入一系列局部時(shí)鐘變量來(lái)分別記錄各個(gè)中斷處理任務(wù)的執(zhí)行時(shí)間，并通過(guò)停表機(jī)制來(lái)支持高優(yōu)先級(jí)中斷的處理任務(wù)可以隨時(shí)打斷低優(yōu)先級(jí)中斷的處理任務(wù)這一搶占式的調(diào)度策略．停表機(jī)制要求任一時(shí)刻，系統(tǒng)中只有唯一的局部時(shí)鐘變量是活動(dòng)的，而其它局部時(shí)鐘變量保持不變．中斷時(shí)間自動(dòng)機(jī)的主要局限在于它不允許模型中存在全局時(shí)鐘變量，因此無(wú)法滿足為中斷源建模的需要．以本文中系統(tǒng)為例，這一系統(tǒng)是在外部?jī)蓚€(gè)周期性發(fā)生的中斷源驅(qū)動(dòng)下運(yùn)行的．在各種嵌入式控制系統(tǒng)中，這種基于多重控制周期性的控制方法，是被廣泛使用的控制技術(shù)．在對(duì)實(shí)時(shí)控制系統(tǒng)進(jìn)行驗(yàn)證時(shí)，需要同時(shí)對(duì)中斷驅(qū)動(dòng)系統(tǒng)的行為和外部中斷源的行為進(jìn)行建模和處理．顯然，中斷時(shí)間自動(dòng)機(jī)并不能完全滿足這樣的建模和驗(yàn)證要求．

基于上述分析，本文提出了一種基于線性混成自動(dòng)機(jī)理論，為中斷驅(qū)動(dòng)系統(tǒng)及外部中斷源進(jìn)行建模和驗(yàn)證的方法．其基本思想是將線性混成自動(dòng)機(jī)中的變量分為全局時(shí)鐘變量和中斷時(shí)鐘變量?jī)煞N：全局時(shí)鐘變量在任意時(shí)刻的變化率都為1，可以用來(lái)描述系統(tǒng)運(yùn)行時(shí)刻的外部中斷源的行為；而中斷時(shí)鐘變量對(duì)應(yīng)于一個(gè)處理任務(wù)，只在描述該任務(wù)的節(jié)點(diǎn)中具有變化率1而在其他所有的節(jié)點(diǎn)中變化率均為0．對(duì)于一個(gè)中斷驅(qū)動(dòng)系統(tǒng)，可以定義全局時(shí)鐘變量來(lái)描述系統(tǒng)的上下文、刻畫中斷源的行為，描述中斷觸發(fā)；而用中斷時(shí)鐘變量來(lái)描述響應(yīng)中斷請(qǐng)求任務(wù)的行為，進(jìn)而建立整個(gè)系統(tǒng)(中斷驅(qū)動(dòng)系統(tǒng)和中斷源)的行為模型.

在線性混成自動(dòng)機(jī)表達(dá)的行為模型上，系統(tǒng)的時(shí)間約束是否得到滿足，可以轉(zhuǎn)化為驗(yàn)證系統(tǒng)中是否存在不滿足該時(shí)間約束的路徑，即可以將系統(tǒng)的時(shí)間約束驗(yàn)證問(wèn)題轉(zhuǎn)換為線性混成自動(dòng)機(jī)上的路徑可達(dá)性判定問(wèn)題．本文借助模型檢驗(yàn)工具BACH[6,7]對(duì)該路徑的可達(dá)性問(wèn)題進(jìn)行驗(yàn)證．

1 中斷驅(qū)動(dòng)的系統(tǒng)建模

對(duì)于中斷驅(qū)動(dòng)系統(tǒng)，在某一時(shí)刻可能有多個(gè)中斷請(qǐng)求等待響應(yīng)．根據(jù)中斷的優(yōu)先級(jí)，在某一時(shí)刻系統(tǒng)響應(yīng)具有最高優(yōu)先級(jí)的中斷，而將其它的請(qǐng)求放入等待隊(duì)列中．作為應(yīng)用搶占式調(diào)度策略的系統(tǒng)，在中斷驅(qū)動(dòng)系統(tǒng)中，高優(yōu)先級(jí)的中斷可以掛起正在執(zhí)行的低優(yōu)先級(jí)中斷處理任務(wù)而優(yōu)先得到處理；當(dāng)高優(yōu)先級(jí)的中斷處理結(jié)束后，系統(tǒng)會(huì)返回繼續(xù)低優(yōu)先級(jí)中斷請(qǐng)求的處理．中斷觸發(fā)的不可預(yù)測(cè)性使得中斷驅(qū)動(dòng)系統(tǒng)的時(shí)序較復(fù)雜．為了對(duì)中斷驅(qū)動(dòng)系統(tǒng)進(jìn)行形式化描述，可以將其行為描述為系統(tǒng)的行為和外部中斷源的行為兩部分．系統(tǒng)的行為即該中斷驅(qū)動(dòng)系統(tǒng)對(duì)多級(jí)中斷請(qǐng)求的調(diào)度和響應(yīng)，外部中斷源的行為即中斷觸發(fā)的描述，這往往依賴于系統(tǒng)運(yùn)行的上下文環(huán)境．

線性混成自動(dòng)機(jī)是描述既有連續(xù)行為又有動(dòng)態(tài)變化的動(dòng)態(tài)系統(tǒng)的形式化模型，其可達(dá)性問(wèn)題已被證明是不可判定的[8,9]．線性混成自動(dòng)機(jī)的定義如下：

定義1線性混成自動(dòng)機(jī)（Linear Hybrid Automata）

線性混成自動(dòng)機(jī)是一個(gè)八元組，H=(X,Σ,V,V0,E,α,β,γ)，其中：

X={x1···,xn}是一組實(shí)數(shù)變量，n為H的維數(shù)；

Σ是一個(gè)有窮的事件集；

V是位置節(jié)點(diǎn)的有限集；

v0?V是一組初始位置集；

E是一組轉(zhuǎn)換關(guān)系，E中的元素具有形式(v,σ,φ,?,v′)，其中是一組形如b的轉(zhuǎn)換約束表達(dá)式，?是形如x=c的重置變量集，其中，

α是位置集到節(jié)點(diǎn)不變式的映射，其中節(jié)點(diǎn)不變式是一組形為X)的線性表達(dá)式；

β是位置集到變化率集合的映射，其中變化率是形如˙x=[a,b](a,b∈R,x,xi∈X,a≤b)的表達(dá)式．對(duì)于每個(gè)位置節(jié)點(diǎn)，每個(gè)變量有且僅有一個(gè)變化率；

γ是初始位置集v0到初始條件的映射，其中初始條件是形如x=a(x∈X,a∈R)的表達(dá)式．

使用線性混成自動(dòng)機(jī)模型對(duì)實(shí)際系統(tǒng)建模，首先需要抽象時(shí)鐘變量；然后使用基于時(shí)鐘變量的表達(dá)式描述系統(tǒng)的行為約束．為了直觀的描述中斷驅(qū)動(dòng)系統(tǒng)，在此我們將線性混成自動(dòng)機(jī)的變量分為全局時(shí)鐘變量和中斷時(shí)鐘變量?jī)深悾喝謺r(shí)鐘變量在所有節(jié)點(diǎn)的變化率都為1，可以用來(lái)描述系統(tǒng)的上下文環(huán)境；而每個(gè)中斷時(shí)鐘變量都對(duì)應(yīng)一個(gè)特定優(yōu)先級(jí)的任務(wù)，其變化率只在具有當(dāng)前優(yōu)先級(jí)的任務(wù)節(jié)點(diǎn)中為1而在其他節(jié)點(diǎn)中都為0．

對(duì)于一個(gè)中斷驅(qū)動(dòng)系統(tǒng)，首先定義全局時(shí)鐘變量來(lái)描述外部中斷源的行為，即通過(guò)全局時(shí)鐘變量來(lái)控制中斷的觸發(fā)，并根據(jù)系統(tǒng)的實(shí)際運(yùn)行建立基于全局時(shí)鐘變量的表達(dá)式，用來(lái)刻畫中斷請(qǐng)求的觸發(fā)．然后定義中斷時(shí)鐘變量來(lái)描述中斷驅(qū)動(dòng)系統(tǒng)對(duì)中斷請(qǐng)求的調(diào)度和響應(yīng)．一般，對(duì)于每個(gè)優(yōu)先級(jí)的中斷請(qǐng)求，均定義一個(gè)中斷時(shí)鐘變量來(lái)描述系統(tǒng)對(duì)該中斷請(qǐng)求的響應(yīng)，所以一個(gè)中斷時(shí)鐘變量的取值對(duì)應(yīng)于該中斷請(qǐng)求的處理時(shí)間，這樣就可以建立基于中斷時(shí)鐘變量的系統(tǒng)的時(shí)間約束．一般中斷驅(qū)動(dòng)系統(tǒng)中還會(huì)有非中斷任務(wù)在執(zhí)行，對(duì)此可以定義具有低優(yōu)先級(jí)的中斷時(shí)鐘變量來(lái)描述系統(tǒng)對(duì)這些任務(wù)的處理．進(jìn)而根據(jù)系統(tǒng)的行為來(lái)建立描述整個(gè)中斷驅(qū)動(dòng)系統(tǒng)的線性混成自動(dòng)機(jī)模型．下面，以一個(gè)具體案例來(lái)說(shuō)明．

某周期性中斷源驅(qū)動(dòng)的系統(tǒng)在運(yùn)行前試驗(yàn)時(shí)發(fā)生故障．通過(guò)一系列的故障分析和試驗(yàn)驗(yàn)證，得出結(jié)論：發(fā)生故障的原因是在通信過(guò)程中連續(xù)9個(gè)周期發(fā)生錯(cuò)誤，按照預(yù)設(shè)此時(shí)會(huì)導(dǎo)致故障的觸發(fā)．具體的，該系統(tǒng)存在兩級(jí)和故障相關(guān)的中斷：高優(yōu)先級(jí)的0.5s控制周期中斷和低優(yōu)先級(jí)的4s控制周期中斷，在高優(yōu)先級(jí)的中斷觸發(fā)時(shí)，系統(tǒng)需掛起當(dāng)前任務(wù)來(lái)響應(yīng)中斷．0.5s控制周期中斷處理任務(wù)分為長(zhǎng)周期和短周期，響應(yīng)時(shí)間分別為[155,160]和[193,197]．在該系統(tǒng)中，長(zhǎng)短周期處理任務(wù)中斷交替出現(xiàn)；4s控制周期中斷是系統(tǒng)的通信請(qǐng)求，需要先后完成發(fā)送數(shù)據(jù)和接收應(yīng)答參數(shù)兩部分任務(wù)，其中發(fā)送數(shù)據(jù)的響應(yīng)時(shí)間為[345,350]，接收應(yīng)答參數(shù)的響應(yīng)時(shí)間為4.6ms（上述響應(yīng)時(shí)間單位均為ms）．根據(jù)系統(tǒng)的預(yù)設(shè)行為，若在通信過(guò)程中接收應(yīng)答參數(shù)時(shí)被中斷——即此時(shí)高優(yōu)先級(jí)的0.5s控制周期中斷觸發(fā)，則會(huì)導(dǎo)致此次通信錯(cuò)誤．若在連續(xù)9個(gè)4s周期中均發(fā)生通信錯(cuò)誤，則會(huì)導(dǎo)致系統(tǒng)故障．

圖1 某中斷驅(qū)動(dòng)系統(tǒng)的線性混成自動(dòng)機(jī)模型

分析該系統(tǒng)進(jìn)行建模，首先該中斷驅(qū)動(dòng)系統(tǒng)包含兩級(jí)中斷，即0.5s控制周期中斷和4s控制周期中斷，所以定義兩個(gè)中斷時(shí)鐘變量x1、x2來(lái)分別描述系統(tǒng)對(duì)兩級(jí)中斷的響應(yīng)．同時(shí)，定義中斷時(shí)鐘變量x0來(lái)描述該系統(tǒng)的空閑行為，空閑任務(wù)的優(yōu)先級(jí)最低．接著，定義全局時(shí)鐘變量來(lái)描述中斷源．對(duì)于周期性觸發(fā)的中斷源，考慮到簡(jiǎn)化約束表達(dá)式，可以針對(duì)每個(gè)中斷源都定義一個(gè)全局時(shí)鐘變量gi．當(dāng)gi=ci時(shí)，其中ci為該級(jí)中斷的控制周期，則會(huì)觸發(fā)具有該優(yōu)先級(jí)的中斷；若該中斷請(qǐng)求的優(yōu)先級(jí)較當(dāng)前正在處理的任務(wù)的優(yōu)先級(jí)高，則系統(tǒng)會(huì)掛起當(dāng)前的任務(wù)來(lái)響應(yīng)中斷．抽象系統(tǒng)的行為，該中斷驅(qū)動(dòng)系統(tǒng)的線性混成自動(dòng)機(jī)模型如圖1所示．其中，q0為初始狀態(tài)，q1，q5描述0.5s控制周期中斷的短周期和長(zhǎng)周期任務(wù)處理，對(duì)應(yīng)優(yōu)先級(jí)最高的中斷時(shí)鐘變量為x2；q2，q4分別描述4s控制周期的通信處理任務(wù)中發(fā)送數(shù)據(jù)和接收參數(shù)，對(duì)應(yīng)的中斷時(shí)鐘變量為x1，其優(yōu)先級(jí)較x2低而比x0高；q3、q6為空閑狀態(tài)，具有最低優(yōu)先級(jí)的時(shí)鐘變量x0描述其行為．

根據(jù)案例中的描述，系統(tǒng)在通信過(guò)程中，若在接收參數(shù)時(shí)被中斷，即發(fā)生了高優(yōu)先級(jí)的中斷，則會(huì)導(dǎo)致此次通信錯(cuò)誤．對(duì)應(yīng)于該線性混成自動(dòng)機(jī)模型中，即出發(fā)于q4節(jié)點(diǎn)的轉(zhuǎn)換是由于高優(yōu)先級(jí)的中斷觸發(fā)（此時(shí)g1==500），此時(shí)在q4節(jié)點(diǎn)的停留時(shí)間必然小于4.6ms（對(duì)應(yīng)于500≤x1＜504.6），系統(tǒng)發(fā)生通信錯(cuò)誤．所以若在某次運(yùn)行時(shí)發(fā)生轉(zhuǎn)換，則系統(tǒng)發(fā)生通信錯(cuò)誤．若在連續(xù)9個(gè)4s控制周期中均觸發(fā)該轉(zhuǎn)換，則系統(tǒng)發(fā)生故障．

2 時(shí)間約束的驗(yàn)證方法

前面已提及，線性混成自動(dòng)機(jī)可達(dá)性問(wèn)題是不可判定的，現(xiàn)有的對(duì)線性混成自動(dòng)機(jī)完整狀態(tài)空間一些嘗試驗(yàn)證，或者可以解決的問(wèn)題規(guī)模很小，效果頗為有限，或者模型本身有太多的約束．在[10]中，作者針對(duì)線性混成自動(dòng)機(jī)的有界可達(dá)性驗(yàn)證問(wèn)題提出了面向路徑的有效解決方法，即對(duì)線性混成自動(dòng)機(jī)中的一條路徑編碼得到一組線性約束，進(jìn)而利用線性規(guī)劃技術(shù)來(lái)判斷該路徑是否可達(dá)．

給定線性混成自動(dòng)機(jī)對(duì)于形如的位置序列，若對(duì)任意的i(0≤i≤n)，序列(vi,σi,?i,Ψi,vi+1)∈E，則稱ρ為H的一條路徑．針對(duì)路徑ρ對(duì)每個(gè)位置節(jié)點(diǎn)添加一個(gè)非負(fù)實(shí)數(shù)δi(0≤i≤n)，可以得到該路徑的一個(gè)時(shí)間序列

定義2給定線性混成自動(dòng)機(jī)

H=(X,Σ,V,v0,E,α,β,γ)的時(shí)間序列若該序列滿足下述條件，則該序列表示H的一個(gè)行為：

H存在路徑:

δ1，δ2，···，δn滿足轉(zhuǎn)換約束?i(0≤i≤n?1)中的所有變量約束；δ1，δ2，···，δn滿足任意位置節(jié)點(diǎn)vi(0≤i≤n)的節(jié)點(diǎn)不變式．

定義3給定線性混成自動(dòng)機(jī)H中的路徑及可達(dá)性約束(v,φ)，H基于ρ的行為滿足R(v,φ)，當(dāng)且僅當(dāng)v=v該

n行為滿足φ的所有變量約束．

基于上述定義，給定線性混成自動(dòng)機(jī)H中的路徑及可達(dá)性約束R(v,φ)，若ρ滿足R(v,φ)，則必然存在行為滿足R(v,φ)．那么，δ1，δ2，···，δn必然同時(shí)滿足?i,α(vi)(0≤i≤n)以及φ中的所有變量約束．以上條件構(gòu)成了關(guān)于變量δ1，δ2，···，δn的一組線性不等式θ(ρ,R(v,φ))．若θ(ρ,R(v,φ))有解，那么就存在一組δ1，δ2，···，δn構(gòu)成滿足R(v,φ)的自動(dòng)機(jī)行為．這就是[10]面向路徑的可達(dá)性驗(yàn)證的基本原理．

基于上述理論，在[6,7]中，作者描述了一個(gè)面向線性混成系統(tǒng)有界可達(dá)模型檢驗(yàn)工具BACH（Boundedre AcheabilityCHecker）．BACH集合線性混成自動(dòng)機(jī)圖形編輯器、文本編輯器和線性混成自動(dòng)機(jī)可達(dá)性驗(yàn)證工具集，提供了針對(duì)線性混成自動(dòng)機(jī)的有界可達(dá)驗(yàn)證，包括面向路徑的可達(dá)性驗(yàn)證和有界可達(dá)性驗(yàn)證．

對(duì)于要驗(yàn)證的時(shí)間約束相關(guān)性質(zhì)，首先需要將其在系統(tǒng)模型中描述出來(lái)，這可以通過(guò)定義滿足該性質(zhì)的節(jié)點(diǎn)或是轉(zhuǎn)換來(lái)實(shí)現(xiàn)，這樣就將系統(tǒng)的時(shí)間約束判定問(wèn)題轉(zhuǎn)換為線性混成自動(dòng)機(jī)的可達(dá)性問(wèn)題．進(jìn)而，根據(jù)系統(tǒng)的行為找到描述該性質(zhì)的路徑，借助面向路徑的可達(dá)性驗(yàn)證技術(shù)來(lái)判定該路徑是否可達(dá)，即判定該時(shí)間約束性質(zhì)是否被滿足．下面以上一節(jié)介紹的周期性中斷源驅(qū)動(dòng)的嵌入式系統(tǒng)為例，來(lái)說(shuō)明如何借助BACH的面向路徑的可達(dá)性驗(yàn)證功能，來(lái)驗(yàn)證系統(tǒng)是否會(huì)發(fā)生故障，即存在某次執(zhí)行在連續(xù)9個(gè)4s控制周期中均發(fā)生通信錯(cuò)誤．

首先需要定義描述該性質(zhì)的節(jié)點(diǎn)或是轉(zhuǎn)換．考慮到該系統(tǒng)是一個(gè)周期性中斷源驅(qū)動(dòng)的系統(tǒng)，所以可以先建立一個(gè)周期上的性質(zhì)描述，即在一個(gè)控制周期中系統(tǒng)發(fā)生通信錯(cuò)誤．對(duì)于該系統(tǒng)，一次4s控制周期中斷的處理加0.5s控制周期中斷的長(zhǎng)周期和短周期任務(wù)處理所需要的時(shí)間為[698.6ms,711.6ms]，即在第三個(gè)0.5s控制周期中斷觸發(fā)之前就可以結(jié)束4s中斷處理任務(wù)，因此只需要分析系統(tǒng)的在最開始的1s中的行為．根據(jù)前面的分析可得若在某次執(zhí)行中觸發(fā)則會(huì)發(fā)生通信錯(cuò)誤．所以，轉(zhuǎn)換關(guān)系描述了一個(gè)周期中的時(shí)間約束性質(zhì)，即通信錯(cuò)誤的發(fā)生．

繼而需要找到描述該時(shí)間約束性質(zhì)的路徑．分析該系統(tǒng)的行為可知，始于q4的轉(zhuǎn)換都是安全的．這主要是因?yàn)檫@些轉(zhuǎn)換都是在第二個(gè)0.5s控制周期中斷觸發(fā)或者在等待該次觸發(fā)時(shí)的轉(zhuǎn)換，所以在一個(gè)周期的執(zhí)行中，這四個(gè)轉(zhuǎn)換有且只有一個(gè)會(huì)被觸發(fā)．至此可以得到在一個(gè)周期中系統(tǒng)發(fā)生通信錯(cuò)誤的路徑（根據(jù)系統(tǒng)的行為，可以容易的放棄其他路徑由于在該系統(tǒng)中，轉(zhuǎn)換關(guān)系描述了系統(tǒng)在一個(gè)周期后的重置上下文，所以對(duì)于性質(zhì)——連續(xù)9個(gè)周期均發(fā)生通信錯(cuò)誤，可以通過(guò)重復(fù)一個(gè)周期里的行為來(lái)描述．上述待驗(yàn)證的路徑在BACH中可描述為：

使用BACH online版本BACHOL，在PC（Intel Core2 Quad CPU 2.66G Hz/RAM 4.00G，Java 1.7.0）上對(duì)前面得到的模型和路徑進(jìn)行驗(yàn)證．在面向路徑的可達(dá)性驗(yàn)證功能中，可以在reachability specif i cation選項(xiàng)中添加該待驗(yàn)證路徑在最后一個(gè)位置節(jié)點(diǎn)要滿足的規(guī)約．在此，針對(duì)該中斷驅(qū)動(dòng)系統(tǒng)的待驗(yàn)證性質(zhì)，我們只需要驗(yàn)證上述路徑是否可達(dá)，沒有額外的規(guī)約需要滿足．添加系統(tǒng)模型，在路徑（path）選項(xiàng)中添加待驗(yàn)證的路徑，經(jīng)1.5s左右，可得實(shí)驗(yàn)結(jié)果如圖2：滿足可達(dá)性約束．即上述路徑是可達(dá)的．對(duì)應(yīng)該中斷驅(qū)動(dòng)系統(tǒng)的描述，其存在發(fā)生故障的風(fēng)險(xiǎn)．

圖2 實(shí)驗(yàn)結(jié)果

3 相關(guān)工作比較和討論

對(duì)中斷驅(qū)動(dòng)系統(tǒng)的時(shí)間約束的保證，傳統(tǒng)的以測(cè)試為基礎(chǔ)的方法無(wú)法完全遍歷系統(tǒng)的整個(gè)運(yùn)行軌跡空間，其有效性受到很大的限制．同時(shí)，測(cè)試的代價(jià)是相當(dāng)昂貴的．

隨著自動(dòng)驗(yàn)證技術(shù)的應(yīng)用，通過(guò)構(gòu)造系統(tǒng)的行為模型、借助現(xiàn)有的驗(yàn)證工具來(lái)驗(yàn)證系統(tǒng)的時(shí)間約束性質(zhì)成為主要的研究方向．在[1]中，作者應(yīng)用模型驗(yàn)證理論，對(duì)兩個(gè)調(diào)度協(xié)議ICPP（Immediate Ceiling Priority Protocol(ICPP)）和EDF（Earliest Deadline First）建立時(shí)間自動(dòng)機(jī)模型，利用驗(yàn)證工具UPPAAL驗(yàn)證了互斥訪問(wèn)、優(yōu)先調(diào)度等正確性相關(guān)性質(zhì)．但這只是驗(yàn)證協(xié)議本身來(lái)保證調(diào)度協(xié)議的正確性，文中的實(shí)例驗(yàn)證也只是保證在該調(diào)度下系統(tǒng)的功能性需求，而沒有給出在該調(diào)度下系統(tǒng)滿足時(shí)間約束相關(guān)性質(zhì)的驗(yàn)證方法．而在[2]中，作者針對(duì)滿足固定優(yōu)先級(jí)理論假設(shè)的實(shí)時(shí)系統(tǒng)，建立用最壞完成時(shí)間（Worst-Case Completion Time）來(lái)約束轉(zhuǎn)換的時(shí)間自動(dòng)機(jī)模型，利用KRONOS工具來(lái)驗(yàn)證任務(wù)的響應(yīng)時(shí)間是否滿足實(shí)際需求、不同任務(wù)所需時(shí)間的關(guān)系以及任務(wù)調(diào)度間的相關(guān)性等性質(zhì)．在[3]中，作者針對(duì)使用非優(yōu)先級(jí)調(diào)度的分布實(shí)時(shí)嵌入式系統(tǒng)提出了一套驗(yàn)證體系DREAM（Distributed Real-time Embedded Analysis Method）．DREAM允許使用DML（Domain Modeling Language）直接描述模型，然后利用模型轉(zhuǎn)換將其轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)模型，將調(diào)度問(wèn)題轉(zhuǎn)換為時(shí)間自動(dòng)機(jī)的可達(dá)性問(wèn)題，進(jìn)而借助現(xiàn)有的模型檢驗(yàn)工具來(lái)檢驗(yàn)在該調(diào)度下任務(wù)的完成時(shí)間是否滿足系統(tǒng)的需求等性質(zhì)．這些基于時(shí)間自動(dòng)機(jī)理論的方法都要求系統(tǒng)的任務(wù)調(diào)度是不可搶占的，即一個(gè)任務(wù)必須在一次執(zhí)行中完成而不允許被新的任務(wù)中斷；而對(duì)于應(yīng)用搶占式調(diào)度策略的中斷驅(qū)動(dòng)系統(tǒng)，其一次中斷任務(wù)的響應(yīng)可能會(huì)多次被高優(yōu)先級(jí)的中斷響應(yīng)掛起，只有在高優(yōu)先級(jí)的中斷任務(wù)處理結(jié)束后方返回繼續(xù)響應(yīng)該請(qǐng)求，這無(wú)法通過(guò)普通時(shí)鐘變量來(lái)描述——普通時(shí)鐘變量只能描述任務(wù)一次執(zhí)行行為的時(shí)間約束，而無(wú)法刻畫可以被多次打斷的可搶占中斷驅(qū)動(dòng)系統(tǒng)的時(shí)間約束．

此外，還有一些基于Petri網(wǎng)的實(shí)時(shí)系統(tǒng)調(diào)度研究[4]．Petri網(wǎng)主要用來(lái)描述系統(tǒng)的動(dòng)態(tài)行為，應(yīng)用時(shí)間Petri網(wǎng)可以為一個(gè)轉(zhuǎn)換的觸發(fā)添加時(shí)間約束，來(lái)描述在轉(zhuǎn)換前的位置的停留時(shí)間．基于時(shí)間Petri網(wǎng)的實(shí)時(shí)系統(tǒng)的調(diào)度研究，所能描述的系統(tǒng)調(diào)度也是不可搶占的，所以仍然無(wú)法對(duì)應(yīng)用搶占式調(diào)度策略的中斷驅(qū)動(dòng)系統(tǒng)進(jìn)行建模．

在[5]中，作者提出一種新的混成自動(dòng)機(jī)的子類——中斷時(shí)間自動(dòng)機(jī)（Interrupt Timed Automata，ITA）來(lái)描述中斷驅(qū)動(dòng)系統(tǒng)．在中斷時(shí)間自動(dòng)機(jī)中，每個(gè)節(jié)點(diǎn)都被賦予一個(gè)優(yōu)先級(jí)，在每個(gè)節(jié)點(diǎn)中只有具有當(dāng)前優(yōu)先級(jí)的時(shí)鐘變量執(zhí)行，即其所謂的中斷時(shí)鐘，來(lái)描述具有該優(yōu)先級(jí)的中斷請(qǐng)求的行為．此外，對(duì)轉(zhuǎn)換關(guān)系中更新函數(shù)的約束使得中斷時(shí)鐘可以準(zhǔn)確的描述具有當(dāng)前中斷優(yōu)先級(jí)的中斷任務(wù)的處理情況．中斷時(shí)間自動(dòng)機(jī)可以直觀的描述應(yīng)用搶占式調(diào)度策略的中斷驅(qū)動(dòng)系統(tǒng)的行為，作為線性混成自動(dòng)機(jī)的子類，只允許定義中斷時(shí)鐘變量的約束使得其避免了線性混成自動(dòng)機(jī)可達(dá)性問(wèn)題的不可判定性：中斷時(shí)間自動(dòng)機(jī)的可達(dá)性問(wèn)題的復(fù)雜度為NEXPTIME，在時(shí)鐘變量數(shù)確定時(shí)復(fù)雜度為PTIME．但只允許定義中斷時(shí)鐘變量而無(wú)法定義普通時(shí)鐘變量的約束，使得在中斷時(shí)間自動(dòng)機(jī)中無(wú)法定義全局時(shí)鐘；而外部中斷源的行為一般是獨(dú)立于系統(tǒng)行為而依賴于全局時(shí)鐘的變化，所以中斷時(shí)間自動(dòng)機(jī)模型對(duì)外部中斷源的行為的描述有限．對(duì)前面案列中描述的中斷驅(qū)動(dòng)系統(tǒng)，其周期性中斷源的行為就無(wú)法通過(guò)中斷時(shí)鐘變量來(lái)描述：無(wú)法通過(guò)中斷時(shí)鐘變量來(lái)獲得系統(tǒng)的全局時(shí)鐘．顯然中斷時(shí)間自動(dòng)機(jī)并不能完全滿足同時(shí)對(duì)中斷驅(qū)動(dòng)系統(tǒng)的行為和外部中斷源的行為進(jìn)行建模和處理的需要．

上述分析表明，針對(duì)非搶占式系統(tǒng)的驗(yàn)證工作無(wú)法描述中斷驅(qū)動(dòng)系統(tǒng)中高優(yōu)先級(jí)中斷處理任務(wù)可以隨時(shí)打斷低優(yōu)先級(jí)中斷處理任務(wù)這一基本行為模式．而中斷時(shí)間自動(dòng)機(jī)由于不支持全局時(shí)間變量，無(wú)法滿足對(duì)中斷源進(jìn)行建模的需求．本文提出的基于線性混成自動(dòng)機(jī)對(duì)中斷驅(qū)動(dòng)系統(tǒng)進(jìn)行建模的方法，可以很好地滿足中斷驅(qū)動(dòng)系統(tǒng)的這兩個(gè)基本驗(yàn)證需求．

4 結(jié)論和進(jìn)一步工作

本文針對(duì)中斷驅(qū)動(dòng)系統(tǒng)提出了一種基于線性混成自動(dòng)機(jī)有界可達(dá)性驗(yàn)證的時(shí)間約束驗(yàn)證方法．首先通過(guò)抽象中斷驅(qū)動(dòng)系統(tǒng)的中斷時(shí)鐘變量來(lái)描述中斷的響應(yīng)行為，抽象普通時(shí)鐘變量來(lái)刻畫中斷的觸發(fā)，建立中斷驅(qū)動(dòng)系統(tǒng)的線性混成自動(dòng)機(jī)模型來(lái)描述系統(tǒng)的行為；進(jìn)而應(yīng)用線性混成自動(dòng)機(jī)的有界可達(dá)性驗(yàn)證和模型檢驗(yàn)工具BACH來(lái)驗(yàn)證系統(tǒng)的時(shí)間約束相關(guān)性質(zhì)．同時(shí)以一個(gè)周期性中斷源驅(qū)動(dòng)的嵌入式系統(tǒng)為例，通過(guò)找到與時(shí)間約束相關(guān)的路徑，利用BACH的面向路徑可達(dá)性驗(yàn)證功能，來(lái)驗(yàn)證該性質(zhì)是否被滿足．

目前的研究工作需要設(shè)計(jì)人員在混成自動(dòng)機(jī)模型上手動(dòng)標(biāo)記出待驗(yàn)證的路徑．如果模型中存在多條路徑對(duì)應(yīng)于待驗(yàn)證的性質(zhì)，手動(dòng)標(biāo)記出所有路徑的過(guò)程會(huì)比較困難且易出錯(cuò)．今后研究工作的重要方面是擴(kuò)展BACH工具的有界驗(yàn)證功能，使其能夠自動(dòng)找出給定邊界內(nèi)所有的路徑，并對(duì)這些路徑是否滿足時(shí)間約束進(jìn)行驗(yàn)證，從而免去用戶手動(dòng)標(biāo)記路徑的工作，提高這一方法的自動(dòng)化水平和有效性．

參考文獻(xiàn)：

[1]Gerdsmeier T,Cardell-Oliver R.Analysis of scheduling behaviour using generic timed automata[J].Electronic Notes in Theoretical Computer Science,2001,42:143-157.

[2]Braberman V A,Felder M.Verif i cation of real-time designs:Combining scheduling theory with automatic formal verif i cation[J].Software Engineering-ESEC/FSE,1999,99:494-510.

[3]Madl G,Abdelwahed S,andSchmidt D.Verifying distributed real-timeproperties of embedded systems via graph transformations and modelchecking[J].Real-Time Systems,2006,33(1-3):77-100.

[4]Cortes L A,Eles P,Peng Z.Modeling and formal verif i cation of embedded systems based on a Petri net representation[J].Journal of Systems Architecture:the EUROMICRO Journal,2003,49(12-15):571-598.

[5]B′erard B,Haddad S,Sassolas M.Interrupt timed automata:verif i cation and expressiveness[J].Formal Methods in System Design,2012,40(1):41-87.

[6]Bu L,Li Y,Wang L,et al.BACH:Bounded reachability checker for linear hybrid automata[C]//In:Cimatti A,Jones R,eds.Proc.of the 8th Int’l Conf.on Formal Methods in Computer Aided Design.IEEE Computer Society Press,2008:65-68.

[7]Bu L,Li Y,Wang L Z,et al.BACH:A Toolset for Bounded Reachability Analysis of Linear Hybrid Systems[J].Journal of Software,2011,22(4):640-658.

[8]Henzinger T.The theory of hybrid automata[C]//In:Proc.of the 11th Annual IEEE Symp.on Logic in Computer Science.IEEE Computer Society Press,1996:278-292.

[9]Henzinger T,Kopke PW,Puri A,et al.What’s decidable about hybrid automata[J].Journal of Computer and System Sciences,1998,57(1):94-124.

[10]Li X,Sumit J,Bu L.Towards an eきcient path-oriented tool for bounded reachabilityanalysis of linear hybrid systems using linear programming[J].Electronic Notes in Theoretical Computer Science,2007,174:57-70.

[11]Bu L,Xie DB.Formal verif i cation of hybrid system[J].Journal of Software，2014,25(2):219-233

[12]Huang Yanhong,He Jifeng,Zhu Huibiao.Semantic theories of programs with nested interrupts[J].Frontiers of Computer Science,2015,9(3):331-345.

[13]Zhu H,Yang F,He J,et al.Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language[J].The Journal of Logic and Algebraic Programming,2012,81:2-25