一種基于System C語言的模型檢測方法*

吳麗佳，于 瓊，靳慶庚

(廣西民族大學(xué) 廣西混雜計算與集成電路設(shè)計分析重點實驗室，廣西 南寧 530006)

?

一種基于System C語言的模型檢測方法*

吳麗佳，于 瓊，靳慶庚

(廣西民族大學(xué) 廣西混雜計算與集成電路設(shè)計分析重點實驗室，廣西 南寧 530006)

System C語言在軟硬件協(xié)同設(shè)計過程中被廣泛用來建模和仿真.筆者提出了一種驗證System C設(shè)計的方法，即通過把System C設(shè)計映射成為一個具有良好定義語義的UPPAAL時間自動機.System C設(shè)計的結(jié)構(gòu)和非正式定義的行為在形成的UPPAAL時間自動機中得到了完整的保留.產(chǎn)生的UPPAAL模型允許使用UPPAAL模型檢查器和其配套工具來進行驗證.模型檢查器用來驗證設(shè)計的一些重要屬性，比如活性，死鎖問題和時間約束屬性.通過對兩個實例的活性、安全性和時間屬性的驗證來證明該方法的適用性.

System C；時間自動機；模型檢測

1 System C語言介紹

System C[1-3]語言是一種系統(tǒng)級的硬件描述語言，它繼承和擴展了C++，這使得它可以建模不同抽象級別的包括軟件和硬件的復(fù)雜電子系統(tǒng)，它既可以描述純功能模型和系統(tǒng)體系結(jié)構(gòu)，也可以描述軟硬件的具體實現(xiàn)，但核心是進行電子系統(tǒng)級設(shè)計、建模和驗證[2].System C具有所有硬件描述語言所共有的基本特征，包括模塊、進程、端口和信號等.

一個System C設(shè)計的仿真語義可以總結(jié)為以下幾個步驟：1)初始化：每個進程被執(zhí)行一次；2)求值：所有待執(zhí)行的進程以順序被執(zhí)行；3)更新：原始通道被更新；4)如果有△延遲通知，則相應(yīng)的進程被觸發(fā)并重復(fù)步驟2)和3)；5)如果有定時時間通知則仿真時間被推進到響應(yīng)的定時通知并且重復(fù)步驟2)～4)；6)如果沒有定時事件通知則仿真結(jié)束.

2 UPPAAL時間自動機介紹

時間自動機，就是在傳統(tǒng)有限狀態(tài)機的基礎(chǔ)上增加了時間約束的概念[6],通過用于時鐘約束來建模時間依賴行為的時鐘變量來闡述時間的概念.系統(tǒng)包含多個并發(fā)進程，這些并發(fā)進程由多個時間自動機來建模，然后通過交叉語義被執(zhí)行并且在通道上保持同步.UPPAAL[4-5]是一系列工具的結(jié)合，包含仿真，動態(tài)演示和對多個時間自動機所構(gòu)成的網(wǎng)絡(luò)結(jié)構(gòu)模型的驗證.UPPAAL模型檢查器能夠?qū)r間屬性包括活性和安全性進行驗證.模擬器可用于可視化模型檢查器產(chǎn)生的反例.

3 轉(zhuǎn)化設(shè)計

在本章中描述了我們是如何把System C語言元素轉(zhuǎn)化為時間自動機以及如何把這些映射嵌入完整的設(shè)計的轉(zhuǎn)化中去的，這種轉(zhuǎn)化保留了System C設(shè)計的行為語義和給定的System C設(shè)計的結(jié)構(gòu).該方法要求兩個微小的限制，第一，不能處理動態(tài)進程或者對象的創(chuàng)建，這不會使方法的適用性變得狹窄.第二，UPPAAL只支持有界整型變量.

3.1 方法轉(zhuǎn)化

可執(zhí)行的System C代碼是完全包含在方法內(nèi)的，每一個方法被轉(zhuǎn)化為一個獨立的時間自動機模型，為了建模調(diào)用-返回語句的語義，運用一個同步通道m(xù)_ctrl，如圖1所示.給出的兩個自動機表達了傳統(tǒng)的調(diào)用-返回語義，左邊的調(diào)用者用信號m_ctrl!來手動控制被調(diào)用者，等待被調(diào)用者的方法主體被執(zhí)行，然后在接收到m_ctrl?時繼續(xù)執(zhí)行下一步.圖1展示了一個參數(shù)m_param和一個返回值m_result是如何被傳入給方法的.

圖1 方法轉(zhuǎn)化

方法主體是一系列的聲明的集合，例如return，arithmetic，if-else，while，continue，break和method call.對于每一個聲明我們都附加了轉(zhuǎn)化和位置.接下來，在轉(zhuǎn)化的每一步用術(shù)語 current location來參考最后的附加的位置.我們也保留著初始位置的引用，如果到達一個返回狀態(tài)，會把當(dāng)前狀態(tài)和初始狀態(tài)連接起來并且把這個轉(zhuǎn)化標(biāo)記為m_ctrl!,并且賦值給返回值,如圖1所示.返回狀態(tài)會終止當(dāng)前塊的轉(zhuǎn)化，并且隨后的代碼不會被執(zhí)行.在自動機模型中采用算術(shù)表達式作為更新的條件，因此把當(dāng)前位置定為緊急位置并添加了算術(shù)語句作為轉(zhuǎn)換條件，當(dāng)達到這個條件時執(zhí)行更新操作并轉(zhuǎn)移到下一個位置.為了轉(zhuǎn)化if-else語句增加額外兩條邊，如圖2所示，其中一條邊用if條件來標(biāo)記，另外一條邊用if的否定條件來標(biāo)記.我們把當(dāng)前位置定位緊急位置是因為if條件的判斷不需要時間.把if語句塊添加到if位置上，并且把else語句塊添加到else位置上.如果其他的分支沒有其他的返回語句，則轉(zhuǎn)移到新的當(dāng)前位置.如果其他分支有返回語句，使用其他分支的最后節(jié)點作為新的當(dāng)前位置.如果所有分支都有返回語句則當(dāng)前塊的轉(zhuǎn)化終止.對while循環(huán)的建模和if-else語句類似，如圖2所示；循環(huán)體的語句被附加在滿足while條件的位置上，對于返回語句，當(dāng)前位置和初始位置連接起來，對于continue語句附加在while_begin位置上，break語句附加在while_end位置上.

圖2 if-else和while循環(huán)轉(zhuǎn)化

3.2 調(diào)度機

System C 設(shè)計的執(zhí)行是由調(diào)度機來控制的.進程是最基本的執(zhí)行單元，調(diào)度機的執(zhí)行基于△周期，一個△周期包含求值和更新兩個階段.一個求值和更新循環(huán)構(gòu)成了一個△周期.在求值階段，處于就緒狀態(tài)的進程按隨機順序執(zhí)行，在更新階段，原始通道通過獲得新的值來更新.

用來建模調(diào)度機的時間自動機模型如圖3所示.UPPAAL暗含了初始化操作，在主要仿真循環(huán)前，進程和方法都執(zhí)行一次.我們也可以處理非初始化情況，但是這遺漏了空間限制的情況.調(diào)度機開始求值階段時，通過evaluate位置來刻畫求值階段，如果有處于就緒狀態(tài)的進程，則調(diào)度機會發(fā)送一個激活事件activate!，處于就緒狀態(tài)的進程收到激活事件時開始執(zhí)行.為了保證一次只有一個進程被執(zhí)行，我們采用了二進制通道來激活.為了保證調(diào)度機一次只發(fā)送一個激活事件給就緒狀態(tài)的進程，我們創(chuàng)建了一個計數(shù)器ready_procs來控制數(shù)量，當(dāng)被觸發(fā)時則計數(shù)器增加1，當(dāng)掛起的時候則減1，當(dāng)進程被執(zhí)行完的時候則計數(shù)器ready_procs==0；當(dāng)調(diào)度機到達update位置時則開始更新階段，在更新階段，更新請求通過接受激活事件update_start來隨機執(zhí)行.在更新階段，立即通知是不被允許的，如果沒有更多的更新請求，則調(diào)度機進入下一個△周期，也就是下一個位置next_ delta.當(dāng)結(jié)束更新階段時，調(diào)度機會發(fā)送一個delta_delay!事件來通知△延遲通知一個△周期已經(jīng)結(jié)束.如果有△延遲通知，則相應(yīng)的進程立即被觸發(fā)進入就緒狀態(tài)，他們將會在下一個△周期執(zhí)行；如果沒有觸發(fā)任何進程，則ready_procs==0,仿真時間向前推進到最早的定時通知.在System C語言中有兩種定時通知：一種是函數(shù)e.notify(t)，另一種是wait(t).在System C語言中，定時行為完全由調(diào)度機控制，在時間自動機模型中，可能在本地等待一個給定的時間，因此，對包含時間的進程和事件進行建模更合適.在調(diào)度機中等待最早待定定時通知的一種簡單方法就是在有延遲時讓含有定時行為的進程和事件發(fā)送一個同步廣播信號advance_time!.調(diào)度機接收到advance_time?信號然后開始一個新的△周期，即通過定時通知來執(zhí)行進入就緒狀態(tài)的進程.

調(diào)度機的時間自動機模型和System C中的調(diào)度機表現(xiàn)完全一樣.用來控制進程執(zhí)行的二進制通道和更新通道保證了模型檢查器可以考慮到每一種可能的序列.用于表示△周期執(zhí)行的位置是緊急的，因此不消耗仿真時間.計數(shù)器的作用是用來保證掛起的進程被完全執(zhí)行.在事件通知中，堅定位置的作用是保證調(diào)度機中事件觸發(fā)優(yōu)先于狀態(tài)改變.

圖3 調(diào)度機的時間自動機模型

3.3 事件

如果一個事件對象e被其擁有者通知，則那些對此事件敏感的進程恢復(fù)執(zhí)行.System C支持三種類型的時間通知：一種是e.notify(),即相應(yīng)的進程會在當(dāng)前△周期立即被觸發(fā)；第二種是e.notify(0)，即相應(yīng)的進程會在更新原始通道后下一個△周期立即被觸發(fā)；第三種是e.notify(t)，t>0，即相應(yīng)的進程會在給定的時間t后被觸發(fā)；如果一個事件被掛起的通知所通知，則只有最早的通知起作用，這意味著e.notify()不考慮所有的掛起的通知，e.notify(0)不考慮e.notify(t).

我們?yōu)槭录ο蟮慕Ｈ鐖D4所示.

圖4 事件對象的時間自動機模型

建立的時間自動機模板為每一個被給定的System C設(shè)計聲明的事件對象實例化一個模型.同步通道notify_imm，notify，wait和整型變量t是它的模版參數(shù).在最初，事件僅僅等待被通知.如果被立即通知，則接收notify_imm?信號，并且在廣播通道上立即發(fā)送wait!信號.如果一個事件定時通知或者△延遲通知所通知，則接收notify?并且把參數(shù)t拷貝給本地變量ndelay，本地變量ndelay是由延遲通知產(chǎn)生的，并且在同一時間，本地時鐘x被重置，當(dāng)前到達的堅定位置被用于重新初始化變量ndelay和重置時鐘x.接下來我們需要等待三種情況：1)一個立即時間通知覆蓋了所有的當(dāng)前掛起的通知；2)如果ndelay==0，我們接收到了delta_delay?信號；3)當(dāng)前延遲到期，即x==ndelay&&ndelay!=0；接下來發(fā)送wait!信號，并且回到初始位置.當(dāng)一個定時通知期滿時，通過發(fā)送advance_time!信號來通知調(diào)度機開始下一個求值階段.由于廣播通道advance_time!的作用，如果多個事件的延遲到期，則只有第一個advance_time被調(diào)度機接收；就像之前提到的一樣，要想保留System C的語義，調(diào)度機就必須不能在時間通知完成之前開始求值階段.為了保證這條原則，被掛起的事件對象，作為接收者，也需要和advance_time?保持同步；如果它們接收了advance_time?并且在同一時間他們的延遲期滿，即如果x==ndelay，他們會立即觸發(fā)相應(yīng)的掛起的進程，除此之外其他的什么也不發(fā)生.廣播同步的語義保證了延遲期滿的事件在同一個語義步驟中且在調(diào)度機到達求值階段的時候可以到達堅定位置.堅定位置保證了這些事件在下一個語義步驟中是優(yōu)先的.

3.4 進程和敏感度

在System C語言中，進程是最基本的執(zhí)行單位，每一個進程的執(zhí)行都意味著所調(diào)用的函數(shù)被執(zhí)行.在System C中有兩種類型的進程即方法進程和線程，方法進程通常在執(zhí)行時會將方法體從頭到尾執(zhí)行一遍，它由一系列的敏感事件觸發(fā).用于建模一個方法進程的時間自動機模型如圖5左邊所示.線程可以在執(zhí)行過程中被掛起，動態(tài)等待通知事件或者延遲結(jié)束，它只會在仿真開始的時候被觸發(fā)一次.用于開始一個線程的時間自動機模型如圖5右邊所示.

當(dāng)一個進程調(diào)用wait函數(shù)時會被掛起，如果wait()函數(shù)被無參調(diào)用，則它只有等待敏感事件列表中的事件發(fā)生時才會恢復(fù)執(zhí)行；如果進程調(diào)用wait(e)函數(shù)，則它只有在e事件發(fā)生時才會被再次觸發(fā)；如果進程調(diào)用wait(t,e)，則它只有在e事件發(fā)生后等待t時間單位后才會被觸發(fā)；

圖5 進程的時間自動機模板

我們采用同步通道的方法為時間敏感性建模，如圖6所示.調(diào)用wait(e)函數(shù)的模型如圖6左邊所示，它掛起進程，即發(fā)送同步信號deactivate!，減少進程計數(shù)器ready_procs，然后等待被觸發(fā)，即和事件對象的wait通道保持同步；當(dāng)e_wait?信號被接收時，進程增加進程計數(shù)器ready_procs并且等待被調(diào)度機激活.我們也可以處理組合事件，例如e1&e2或者e1|e2.靜態(tài)敏感和動態(tài)敏感類似，但是當(dāng)調(diào)用wait()時，進程會等待敏感表中的一個事件發(fā)生.我們通過等待敏感表中的其中一個事件發(fā)生和在廣播通道上發(fā)送信號sensitive!的方式來為敏感表建模，如圖6右邊圖所示.使用一個堅定位置來保證立即事件通知立即發(fā)生.我們?yōu)榘粋€敏感進程的靜態(tài)敏感表建立的模型如圖6中間圖所示.和動態(tài)敏感表不同的地方是，我們把e_wait?替換為sensitive?.

圖6 敏感事件模型

采用一個特殊的timeout_event來為定時等待建模.每一個進程都有其獨有的timeout_event.調(diào)用wait(t)過程的模型如圖7左圖所示.首先，釋放一個定時通知來啟動超時操作.其次，進程通過和timeout_event_wait?保持同步來等待超時期滿.通過增加一個同步信號e_wait?來擴展時間自動機模型的方式來滿足等待一個事件定時延遲期滿.如圖7右圖所示；為了保證一個timeout_event不覆蓋隨后的定時通知，當(dāng)時間e發(fā)生時我們用一個立即事件通知來覆蓋它.

圖7 定時和敏感事件模型

3.5 通道和模塊

模塊是系統(tǒng)行為的主要載體，而通道則是通信的主要載體.如果原始通道想要在更新階段讓update()函數(shù)被執(zhí)行則需要實現(xiàn)update()函數(shù)并且在求值階段調(diào)用專用函數(shù)request_update().我們用一個時間自動機模型來管理更新請求，如圖8所示.如果request_update?被接收到，則相應(yīng)的通道的update()函數(shù)被調(diào)度機在更新階段調(diào)用.我們通過在時間自動機模型中發(fā)送request_update!信號來為調(diào)用request_update()函數(shù)的過程建模.

圖8 請求更新的時間自動機模型

模塊和通道的轉(zhuǎn)化要求我們采用變量作為全局變量，配置同步通道和參數(shù)聲明以及生成必要的時間自動機模板.在System C設(shè)計中一個模塊或者通道可能會被多次實例化，為了讓方法模板可以多次重復(fù)使用，我們把所有在模塊中可見的聲明作為模版參數(shù).當(dāng)一個模塊或者通道需要被轉(zhuǎn)化時，相應(yīng)的模板就會生成.全局和系統(tǒng)聲明只有在一個模塊或者通道實例化時才會被添加進UPPAAL模型中.接下來從模塊或者通道中生成的模板會用這些聲明來進行實例化；對于模塊或者通道，事件和進程模板會生成一次.然而，模塊中的方法可能會被當(dāng)前進程多次使用.因此，對于每一個在模塊中聲明過的進程，所有對這個模塊可見的方法都要被實例化一次，相應(yīng)的全局聲明采用模塊名和進程名作為前綴.對于每一個綁定了通道的模塊的每一個進程，通道的成員方法都要被實例化一次.

盡管在UPPAAL中沒有結(jié)構(gòu)層次，但是System C中模塊的結(jié)構(gòu)可以通過前綴體現(xiàn)出來.通過一個System C進程設(shè)計到UPPAAL進程的一對一的映射，System C設(shè)計的結(jié)構(gòu)可以被完全透明的展示給設(shè)計者.這對于模型檢查器生成反例是非常有用的.

4 實驗結(jié)果

我們實現(xiàn)了轉(zhuǎn)化并且自動地將System C設(shè)計轉(zhuǎn)化為UPPAAL模型.采用Karlsruhe System C解析器作為System C設(shè)計的前端.用UPPAAL模型檢查器來驗證設(shè)計的活性和安全性等特性.實驗環(huán)境為Intel 奔騰處理器 3.5 G主頻，操作系統(tǒng)為Linux操作系統(tǒng).第一個實例是生產(chǎn)者消費者協(xié)議；第二個實例是一個經(jīng)過略微修改的信息包交換的實例.在這兩個例子里都包含了System C的通道以及靜態(tài)敏感、動態(tài)敏感和定時敏感的概念.對于生產(chǎn)-消費者實例，我們驗證了以下幾個屬性：1)無死鎖;2)無緩沖區(qū)溢出；3)消費者在給定的時間內(nèi)讀取生產(chǎn)者發(fā)送的所有物品，所有的屬性都可以滿足.對于信息包交換實例，我們驗證了：1)無死鎖;2)每一個信息包都發(fā)往其接收者方向;3)如果一個信息包被發(fā)給其接收者，則在給定時間內(nèi)可以完成.屬性1)和3)都滿足的，屬性2)不能滿足，這是由于sc_signal的語義問題，即當(dāng)值發(fā)生變化時，只有信號端口的改變事件被通知.如果隨后的信息是相同的，則在包交換的輸入端口沒有改變時間發(fā)生，因此只有第一個信息會被發(fā)送給接收者.在生產(chǎn)者消費者實驗中，我們改變了緩沖區(qū)大小(BS 10，BS 50，BS 100，BS 1000)，在包交換實驗中，我們改變了主從服務(wù)器的數(shù)量(1主1從，1主2從，2主1從，2主2從)，表1和表2顯示了10次實驗的驗證時間平均值.

表1 生產(chǎn)-消費者實例實驗結(jié)果

表2 包交換實例實驗結(jié)果

5 總結(jié)

我們提出了一種將System C設(shè)計轉(zhuǎn)化為有著良好定義語義的UPPAAL時間自動機的方法.這種轉(zhuǎn)化可以將UPPAAL工具，包括UPPAAL模型檢查器，應(yīng)用在System C 設(shè)計上，可以形式化驗證System C 設(shè)計的時間屬性.我們主要是將System C 中的進程轉(zhuǎn)化為時間自動機中的進程以及用通道的概念讓它們保持同步.用一個預(yù)定的調(diào)度機模型、特殊的事件模板和進程模板詳細說明了System C設(shè)計的執(zhí)行語義.這種轉(zhuǎn)化可以自動進行且轉(zhuǎn)化時間可以忽略.因此，混合的大型的System C設(shè)計也可以被轉(zhuǎn)化.一個給定的System C設(shè)計的非正式的行為和結(jié)構(gòu)可以被完全的保留在生成的UPPAAL時間自動機模型上.此外，通過我們這種方法產(chǎn)生的模型很簡潔，很容易理解，并且可以有效地被模型檢查器驗證.在將來，我們會優(yōu)化這種的轉(zhuǎn)化，也計劃用生成的模型來自動選擇仿真的輸入以及自動評價仿真的結(jié)果.

[1] T.Groetker.System Design with System C[M].Kluwer Academic Publishers,2002.

[2] A.Habibi and S.Tahar.An Approach for the Verification of SystemC Designs Using AsmL[J].In Automated Technology for Verification and Analysis,2005.

[3] IEEE Standards Association.IEEE Std.1666-2005,Open System C Language Reference Manual[K].2005.

[4]G.Behrmann,A.David,and K.G.Larsen.A Tutorial on UPPAAL.In Formal Methods for the Design of Real-Time Systems[M].LNCS 3185.Springer,2004.

[5]郭華，莊雷.UPPAAL——一種適合自動驗證實時系統(tǒng)的工具[J].微計算機信息，2006(15).

[6]A.Habibi,H.Moinudeen,and S.Tahar.Generating Finite State Machines from System C[M].In Design,Automation and Test in Europe,2006：76-81.

[責(zé)任編輯 蘇 琴]

[責(zé)任校對 黃招揚]

A Method of Model Checking based on System C

WU Li-jia,YU Qiong,JIN Qing-geng

(GuangxiKeyLaboratoryofHybridComputationandICDesignAnalysis,GuangxiUniversityforNationalities,Nanning530006,China)

System C is widely used for modeling and simulation in hardware/software co-design.Due to the lack of a complete formal semantics,it is not possible to verify System C designs.In this paper,we present an approach to overcome this problem by defining the semantics of System C by a mapping from System C designs into the well-defined semantics of UPPAAL timed automata.The informally defined behavior and the structure of System C designs are completely preserved in the generated UPPAAL models.The resulting UPPAAL models allow us to use the UPPAAL model checker and the UPPAAL tool suite,including simulation and visualization tools.The model checker can be used to verify important properties such as liveness,deadlock freedom or compliance with timing constraints.We have implemented the presented transformation,applied it to two examples and verified liveness,safety and timing properties by model checking,thus showing the applicability of our approach in practice.

System C；Timed Automata；Model Checking

2016-03-28.

吳麗佳(1991-)，男，河南許昌人，廣西民族大學(xué)碩士研究生，研究方向：大規(guī)模集成電路驗證.

TP312

A

1673-8462(2016)03-0080-06