為緩解模型檢測的狀態(tài)空間爆炸問題,提出一種基于命題投影時序邏輯的分布式模型檢測方法。通過標記范式圖技術(shù)將命題投影時序邏輯公式描述的待驗證性質(zhì)轉(zhuǎn)換為自動機;根據(jù)強連通分量將其狀態(tài)空間劃分為多個子自動機,將各個子自動機與層次語法圖描述的待驗證系統(tǒng)模型分發(fā)至驗證服務(wù)器集群中,使用動態(tài)驗證技術(shù)進行多機協(xié)同完成系統(tǒng)模型檢測驗證。實驗結(jié)果表明,該方法和單機模型檢測相比驗證時間明顯降低,且能夠驗證更復(fù)雜的系統(tǒng)。 

【文章來源】：西安電子科技大學(xué)學(xué)報. 2020,47(04)北大核心EICSCD

【文章頁數(shù)】：9 頁

【部分圖文】：

命題投影時序邏輯公式p;q的標記范式圖

層次語法圖（Hierarchical Syntax Chart,HSC）是文獻[19]中用來描述面向過程軟件系統(tǒng)執(zhí)行方案語法結(jié)構(gòu)的工具，可通過軟件系統(tǒng)的設(shè)計模型或軟件系統(tǒng)的源碼進行構(gòu)造。層次語法圖將系統(tǒng)的執(zhí)行模型遞歸描述為復(fù)合語句序列，每個復(fù)合語句由復(fù)合語句名稱和復(fù)合語句體構(gòu)成，復(fù)合語句體為語句序列。層次語法圖的結(jié)構(gòu)如圖2所示。第一層為函數(shù)復(fù)合語句，復(fù)合語句名稱（圓形頂點）為函數(shù)名，復(fù)合語句體為函數(shù)體語句（方形頂點）構(gòu)成的語句序列。特別地，當復(fù)合語句體中包含if或while語句時，如函數(shù)Fun1中的if語句，其Yes分支和No分支也分別遞歸描述為復(fù)合語句（while語句結(jié)構(gòu)無No分支）。層次語法圖的形式化定義如下：

命題投影時序邏輯分布式模型檢測采用主從模式的分布式框架，驗證過程如圖3所示。將待驗證系統(tǒng)的層次語法圖模型S和命題投影時序邏輯公式描述的待驗證系統(tǒng)性質(zhì)P輸入到調(diào)度服務(wù)器中，對P使用標記范式圖技術(shù)構(gòu)造性質(zhì)非自動機Ap，然后根據(jù)強連通分量將其狀態(tài)空間劃分為多個子自動機ai p并送入任務(wù)隊列中。調(diào)度服務(wù)器監(jiān)聽各驗證服務(wù)器的狀態(tài)。當存在空閑服務(wù)器時，在任務(wù)隊列中取出一個子自動機ai p和層次語法圖表達的待檢測系統(tǒng)模型S送入該服務(wù)器進行模型檢測驗證，并將驗證結(jié)果返回到調(diào)度服務(wù)器中。下面重點給出狀態(tài)空間劃分算法和模型檢測算法。2.2 性質(zhì)非自動機狀態(tài)空間劃分算法

【參考文獻】：
期刊論文
[1]采用CPAChecker的動態(tài)程序驗證[J]. 段釗,劉錕龍.  西安電子科技大學(xué)學(xué)報. 2019(01)
[2]MSVL程序的自動定理證明方法[J]. 馬倩,段振華.  西安電子科技大學(xué)學(xué)報. 2016(01)
[3]Verilog程序的命題投影時序邏輯符號模型檢測[J]. 逄濤,段振華,劉曉芳.  西安電子科技大學(xué)學(xué)報. 2014(02)
[4]PPTL模型檢測器實現(xiàn)的一個關(guān)鍵技術(shù)[J]. 楊琛,段振華.  西安交通大學(xué)學(xué)報. 2010(10)



本文編號：3495814