吳麗佳，于 瓊，靳慶庚

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

?

一種基于System C語(yǔ)言的模型檢測(cè)方法*

吳麗佳，于 瓊，靳慶庚

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

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

System C；時(shí)間自動(dòng)機(jī)；模型檢測(cè)

1 System C語(yǔ)言介紹

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

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

2 UPPAAL時(shí)間自動(dòng)機(jī)介紹

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

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

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

3.1 方法轉(zhuǎn)化

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

圖1 方法轉(zhuǎn)化

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

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

3.2 調(diào)度機(jī)

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

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

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

圖3 調(diào)度機(jī)的時(shí)間自動(dòng)機(jī)模型

3.3 事件

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

我們?yōu)槭录?duì)象的建模如圖4所示.

圖4 事件對(duì)象的時(shí)間自動(dòng)機(jī)模型

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

3.4 進(jìn)程和敏感度

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

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

圖5 進(jìn)程的時(shí)間自動(dòng)機(jī)模板

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

圖6 敏感事件模型

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

圖7 定時(shí)和敏感事件模型

3.5 通道和模塊

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

圖8 請(qǐng)求更新的時(shí)間自動(dòng)機(jī)模型

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

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

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

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

表1 生產(chǎn)-消費(fèi)者實(shí)例實(shí)驗(yàn)結(jié)果

表2 包交換實(shí)例實(shí)驗(yàn)結(jié)果

5 總結(jié)

我們提出了一種將System C設(shè)計(jì)轉(zhuǎn)化為有著良好定義語(yǔ)義的UPPAAL時(shí)間自動(dòng)機(jī)的方法.這種轉(zhuǎn)化可以將UPPAAL工具，包括UPPAAL模型檢查器，應(yīng)用在System C 設(shè)計(jì)上，可以形式化驗(yàn)證System C 設(shè)計(jì)的時(shí)間屬性.我們主要是將System C 中的進(jìn)程轉(zhuǎn)化為時(shí)間自動(dòng)機(jī)中的進(jìn)程以及用通道的概念讓它們保持同步.用一個(gè)預(yù)定的調(diào)度機(jī)模型、特殊的事件模板和進(jìn)程模板詳細(xì)說(shuō)明了System C設(shè)計(jì)的執(zhí)行語(yǔ)義.這種轉(zhuǎn)化可以自動(dòng)進(jìn)行且轉(zhuǎn)化時(shí)間可以忽略.因此，混合的大型的System C設(shè)計(jì)也可以被轉(zhuǎn)化.一個(gè)給定的System C設(shè)計(jì)的非正式的行為和結(jié)構(gòu)可以被完全的保留在生成的UPPAAL時(shí)間自動(dòng)機(jī)模型上.此外，通過(guò)我們這種方法產(chǎn)生的模型很簡(jiǎn)潔，很容易理解，并且可以有效地被模型檢查器驗(yàn)證.在將來(lái)，我們會(huì)優(yōu)化這種的轉(zhuǎn)化，也計(jì)劃用生成的模型來(lái)自動(dòng)選擇仿真的輸入以及自動(dòng)評(píng)價(jià)仿真的結(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——一種適合自動(dòng)驗(yàn)證實(shí)時(shí)系統(tǒng)的工具[J].微計(jì)算機(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é)任校對(duì) 黃招揚(yáng)]

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ī)模集成電路驗(yàn)證.

TP312

A

1673-8462(2016)03-0080-06