鞠秀芳

(南京大學中國社會科學研究評價中心,江蘇南京210093)

0 引言

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

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

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

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

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

1 中斷驅動的系統(tǒng)建模

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

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

定義1線性混成自動機（Linear Hybrid Automata）

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

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

Σ是一個有窮的事件集；

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

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

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

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

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

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

使用線性混成自動機模型對實際系統(tǒng)建模，首先需要抽象時鐘變量；然后使用基于時鐘變量的表達式描述系統(tǒng)的行為約束．為了直觀的描述中斷驅動系統(tǒng)，在此我們將線性混成自動機的變量分為全局時鐘變量和中斷時鐘變量兩類：全局時鐘變量在所有節(jié)點的變化率都為1，可以用來描述系統(tǒng)的上下文環(huán)境；而每個中斷時鐘變量都對應一個特定優(yōu)先級的任務，其變化率只在具有當前優(yōu)先級的任務節(jié)點中為1而在其他節(jié)點中都為0．

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

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

圖1 某中斷驅動系統(tǒng)的線性混成自動機模型

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

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

2 時間約束的驗證方法

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

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

定義2給定線性混成自動機

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

H存在路徑:

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

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

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

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

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

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

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

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

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

圖2 實驗結果

3 相關工作比較和討論

對中斷驅動系統(tǒng)的時間約束的保證，傳統(tǒng)的以測試為基礎的方法無法完全遍歷系統(tǒng)的整個運行軌跡空間，其有效性受到很大的限制．同時，測試的代價是相當昂貴的．

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

此外，還有一些基于Petri網的實時系統(tǒng)調度研究[4]．Petri網主要用來描述系統(tǒng)的動態(tài)行為，應用時間Petri網可以為一個轉換的觸發(fā)添加時間約束，來描述在轉換前的位置的停留時間．基于時間Petri網的實時系統(tǒng)的調度研究，所能描述的系統(tǒng)調度也是不可搶占的，所以仍然無法對應用搶占式調度策略的中斷驅動系統(tǒng)進行建模．

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

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

4 結論和進一步工作

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

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

參考文獻：

[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