具有程序的靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為語義的時(shí)序邏輯

陳冬火　劉　全,2　金海東　朱　斐,2　王　輝

1(蘇州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院　江蘇蘇州　215006)2　　　(符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué))　長春　130012)

?

具有程序的靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為語義的時(shí)序邏輯

陳冬火1劉全1,2金海東1朱斐1,2王輝1

1(蘇州大學(xué)計(jì)算機(jī)科學(xué)與技術(shù)學(xué)院江蘇蘇州215006)2(符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室(吉林大學(xué))長春130012)

(dhchen@suda.edu.cn)

提出一種區(qū)間分支時(shí)序邏輯——控制流區(qū)間時(shí)序邏輯(control flow interval temporal logic, CFITL)，用于規(guī)約程序的時(shí)序?qū)傩?不同于計(jì)算樹邏輯(computation tree logic, CTL)和線性時(shí)序邏輯(linear temporal logic, LTL)等傳統(tǒng)的時(shí)序邏輯，CFITL公式的語義模型不是基于狀態(tài)的類Kripke結(jié)構(gòu)，而是以程序的抽象模型控制流圖(control flow graph, CFG)為基礎(chǔ)所構(gòu)建的含序CFG結(jié)構(gòu).含序CFG是CFG的一種受限子集，它們的拓?fù)浣Y(jié)構(gòu)可映射為偏序集，這樣誘導(dǎo)產(chǎn)生的自然數(shù)區(qū)間可自然地用于描述定義良好的程序結(jié)構(gòu). 這種結(jié)構(gòu)含有程序的靜態(tài)結(jié)構(gòu)信息和動(dòng)態(tài)行為信息，換而言之，CFITL具有規(guī)約程序?qū)崿F(xiàn)結(jié)構(gòu)屬性和程序執(zhí)行動(dòng)態(tài)行為屬性的能力.在定義CFITL的語法和語義的基礎(chǔ)上，詳細(xì)討論了CFITL的模型檢驗(yàn)問題，包括基于值狀態(tài)空間可達(dá)性計(jì)算的模型檢驗(yàn)方法和基于SMT(satisfiability modulo theories)的CFITL有界模型檢驗(yàn)方法. 現(xiàn)代程序都含有復(fù)雜且具有無限值域的抽象數(shù)據(jù)類型及各種復(fù)雜的操作，CFITL語義定義相比CTL等時(shí)序邏輯更復(fù)雜，因此，基于顯示狀態(tài)搜索的方法難以有效進(jìn)行，而基于SMT的CFITL有界模型檢驗(yàn)方法更易實(shí)現(xiàn)、更具有可行性.最近開發(fā)相關(guān)的原型工具，并進(jìn)行相關(guān)的實(shí)例研究.

區(qū)間時(shí)序邏輯; 控制流程圖; 程序靜態(tài)結(jié)構(gòu)；模型檢驗(yàn)；可滿足性模理論

時(shí)序邏輯是一種模態(tài)邏輯，廣泛用于描述和推理各種計(jì)算機(jī)系統(tǒng)狀態(tài)隨時(shí)間演化所應(yīng)滿足的性質(zhì)，例如計(jì)算樹邏輯(computation tree logic, CTL)[1]、線性時(shí)序邏輯(linear temporal logic, LTL)[2]、概率計(jì)算樹邏輯(probabilistic computation tree logic, PCTL)[3]和連續(xù)時(shí)間隨機(jī)邏輯(continuous time stochastic logic, CSL)[4]等.各種時(shí)序邏輯具有足夠的表達(dá)能力，能用于描述各類計(jì)算機(jī)系統(tǒng)包括安全性屬性及活性屬性的各類性質(zhì).自從20世紀(jì)80年代模型檢驗(yàn)[5]思想提出以來，基于時(shí)序邏輯的模型檢驗(yàn)方法成為形式化驗(yàn)證領(lǐng)域的重要研究方向[6-11].有別于傳統(tǒng)的測試方法，模型檢驗(yàn)方法用算法自動(dòng)檢測系統(tǒng)的行為(數(shù)學(xué)結(jié)構(gòu))是否滿足某條屬性(時(shí)序邏輯公式)，并且當(dāng)系統(tǒng)不滿足相應(yīng)的屬性時(shí)，給出反例作為證據(jù)幫助設(shè)計(jì)者調(diào)試系統(tǒng).對(duì)于系統(tǒng)某個(gè)屬性而言，測試方法通過設(shè)計(jì)測試用例、運(yùn)行系統(tǒng)、觀察輸出等環(huán)節(jié)來驗(yàn)證系統(tǒng)是否滿足這個(gè)屬性，但這種方法是不完備的；而模型檢驗(yàn)方法則通過算法證明系統(tǒng)是否滿足這個(gè)屬性，針對(duì)屬性而言該方法是完備和可靠的.經(jīng)過許多學(xué)者的努力，該方向的研究工作取得了重要的進(jìn)展.除了計(jì)算機(jī)領(lǐng)域的研究人員，各種系統(tǒng)設(shè)計(jì)者和開發(fā)者乃至整個(gè)工業(yè)界都日益重視在軟硬件開發(fā)項(xiàng)目中應(yīng)用時(shí)序邏輯模型檢驗(yàn)方法，以提高所開發(fā)系統(tǒng)功能和性能方面的質(zhì)量[12-16].

傳統(tǒng)的時(shí)序邏輯，例如CTL和LTL，它們的語義模型是基于狀態(tài)，例如Kripke結(jié)構(gòu)[1]，因此它們適合描述狀態(tài)基結(jié)構(gòu)的性質(zhì).在進(jìn)行相應(yīng)的模型檢驗(yàn)時(shí)，不得不建立各種抽象層次的狀態(tài)基模型.時(shí)序邏輯的這種語義定義方法，沒有考慮系統(tǒng)設(shè)計(jì)和實(shí)現(xiàn)的結(jié)構(gòu)因素.此處強(qiáng)調(diào)的結(jié)構(gòu)因素指設(shè)計(jì)和實(shí)現(xiàn)的控制結(jié)構(gòu)，不包括普通意義上的數(shù)據(jù)結(jié)構(gòu)，例如圖1所示程序中的循環(huán)結(jié)構(gòu)和選擇結(jié)構(gòu).但是對(duì)于開發(fā)者而言，在許多情況下，基于系統(tǒng)設(shè)計(jì)和實(shí)現(xiàn)的結(jié)構(gòu)特征描述所開發(fā)系統(tǒng)的屬性是一種更為自然直觀的方式.各種集成開發(fā)環(huán)境所提供的程序點(diǎn)斷言機(jī)制就是一種簡單的基于程序結(jié)構(gòu)的屬性描述方法，更進(jìn)一步，一些語言提供了比程序點(diǎn)斷言更為復(fù)雜的基于結(jié)構(gòu)的屬性描述方法[17-19]，例如Java模型語言(Java modeling language, JML)[20].JML在Java語言的基礎(chǔ)上設(shè)計(jì)了一些特殊語言機(jī)制，可以描述循環(huán)不變式及成員方法輸入和輸出應(yīng)該滿足的條件等，但是這些方法的描述能力具有很大的局限性.對(duì)于圖1所示程序，必須滿足下面4個(gè)屬性：1)對(duì)于任意一條執(zhí)行路徑，數(shù)組b所分配的內(nèi)存資源一定在將來某個(gè)時(shí)刻會(huì)被回收；2)假如返回值為0，則數(shù)組a所有元素的值一定為0；3)在程序點(diǎn)5和程序點(diǎn)9之間屬性i≤a.length∧spot≤a.length為真；4)在程序點(diǎn)5和程序點(diǎn)9之間，若spot≠a.length，則對(duì)于0≤i≤spot,a[i]=0.這些屬性具有顯著的特點(diǎn)：它們都與程序靜態(tài)結(jié)構(gòu)相關(guān)，并且包含動(dòng)態(tài)行為時(shí)序性.

Fig. 1The source code of the function find.

圖1函數(shù)find源代碼

上面的實(shí)例說明構(gòu)造基于系統(tǒng)設(shè)計(jì)和實(shí)現(xiàn)的時(shí)序邏輯系統(tǒng)及設(shè)計(jì)相關(guān)的模型檢驗(yàn)算法具有很大的必要性和價(jià)值.鑒于CTL具有足夠的表達(dá)能力和可判定的邏輯屬性，本文提出一種區(qū)間分支時(shí)序邏輯——控制流區(qū)間時(shí)序邏輯(control flow interval temporal logic, CFITL)，用于描述抽象程序模型——控制流圖(control flow graph, CFG)的時(shí)序性質(zhì).該邏輯的語義解釋集成了程序基于狀態(tài)的執(zhí)行語義及靜態(tài)結(jié)構(gòu)語義，可以描述基于結(jié)構(gòu)和動(dòng)態(tài)行為的各種時(shí)序?qū)傩裕绯绦螯c(diǎn)斷言及循環(huán)結(jié)構(gòu)不變式屬性等.本文在給出CFITL詳細(xì)語法的基礎(chǔ)上，基于CFG的一種受限子集，定義狀態(tài)集的偏序集及相關(guān)的位階函數(shù)rank，用以解釋CFITL公式所涉及的結(jié)構(gòu)因素，進(jìn)而基于符號(hào)狀態(tài)路徑對(duì)CFITL完整的語義進(jìn)行定義.基于可達(dá)狀態(tài)空間計(jì)算的方法討論了CFITL的模型檢驗(yàn)問題.考慮CFITL模型檢驗(yàn)是路徑敏感的，比CTL模型檢驗(yàn)具有更高的復(fù)雜性以及問題域的源程序在數(shù)據(jù)與操作方面的復(fù)雜性，本文基于符號(hào)執(zhí)行技術(shù)[21-23]及時(shí)序邏輯公式重寫技術(shù)[24]定義了CFITL公式的重寫規(guī)則，提出基于可滿足性模理論(satisfiability modulo theories, SMT)[25]的有界模型檢驗(yàn)方法.詳細(xì)設(shè)計(jì)了CFITL模型檢驗(yàn)器的體系架構(gòu)，實(shí)現(xiàn)了原型系統(tǒng)VerTPCFG(verifica-tion of temporal property of CFGs)，實(shí)施相關(guān)的實(shí)例研究，對(duì)所提算法的有效性和效率進(jìn)行初步評(píng)估.

1　控制流區(qū)間時(shí)序邏輯CFITL

控制流區(qū)間時(shí)序邏輯CFITL是計(jì)算樹邏輯CTL的一種擴(kuò)展，通過在語法上引進(jìn)區(qū)間的概念來描述目標(biāo)的結(jié)構(gòu)因素.基于CFITL所描述的屬性把系統(tǒng)基于狀態(tài)的功能性屬性與系統(tǒng)設(shè)計(jì)或?qū)崿F(xiàn)的結(jié)構(gòu)性因素相關(guān)聯(lián).本節(jié)將詳細(xì)介紹該邏輯系統(tǒng)的語法和語義模型.

1.1語法

給定原子命題集合AP及自然數(shù)集合區(qū)間I，下面給出CFITL的抽象語法定義：

ψtrue|p|ψ|ψ1∧ψ2|ψ1∨ψ2|ψ|ψ|

上面抽象語法定義中，p∈AP；和稱為路徑量詞，需要注意的是此處路徑量詞的語義與CTL中量詞的語義有較大的區(qū)別，這一點(diǎn)將在邏輯公式的語義定義中得到說明.，，，是時(shí)序算子，分別表示“下一”、“將來”、“總是”、“直到”的時(shí)間概念. 式中true表示邏輯常量“真”，各種邏輯運(yùn)算符∧，，∨符合標(biāo)準(zhǔn)的邏輯解釋，包括沒有明確定義的邏輯運(yùn)算符→和邏輯真值false.

1.2語義

1.2.1控制流圖和位階函數(shù)

為了使得所定義的邏輯框架不與具體的程序語言相關(guān)，本節(jié)定義程序的抽象模型——控制流圖,該結(jié)構(gòu)將作為CFITL語義解釋的基礎(chǔ).CFG只關(guān)注程序的控制流，忽略程序的數(shù)據(jù)流方面的特性.

定義1. CFG是多元組結(jié)構(gòu)〈Σ,Start,Act,→,Final〉，其中Σ，Start，Act，→，F(xiàn)inal分別解釋如下：

1)Σ是有限的狀態(tài)集合，非空集合Start?Σ為初始狀態(tài)集合，非空集合Final?Σ為終止?fàn)顟B(tài)集合；

2)Act稱為動(dòng)作集合；

令集合Vars為所有程序變量的集合，v∈Vars，Dv表示變量v的取值范圍，V={v1,v2,…,vn}?Vars，DV=Dv1×Dv2×…×Dvn.此處的狀態(tài)集合Σ類似于程序計(jì)數(shù)器，不同于系統(tǒng)的狀態(tài)空間DVars，是抽象的位置標(biāo)示符集合，用來記錄程序的靜態(tài)結(jié)構(gòu)信息.元素l∈Σ被視為字，也即字符串類型. 如果程序模塊具有單入口和單出口的特性，集合Start和Final可用init∈Σ和final∈Σ代替，分別表示開始狀態(tài)和結(jié)束狀態(tài).Act包含2種類型的動(dòng)作：v=e和assume(c)，其中e表示各種滿足程序語言語義約束的運(yùn)算表達(dá)式，c為不含量詞的一階邏輯公式. 需要注意的是，此處的e和c中不含各種可能引進(jìn)副作用的程序表達(dá)式，例如許多程序語言允許v=++x這樣的操作，如果程序出現(xiàn)這種操作，在構(gòu)建程序相關(guān)的CFG時(shí)，應(yīng)把該操作執(zhí)行分解為操作x=x+1和v=x的順序執(zhí)行，并引進(jìn)相應(yīng)的狀態(tài)標(biāo)簽. 符號(hào)序列l(wèi)0a1l1a2…ln-1anln稱為CFG的執(zhí)行路徑，其中?0≤i≤n·li∈Σ,i0∈Start,?1≤j≤n·aj∈Act, ?0≤i≤n-1·〈li,ai+1,li+1〉∈→，此處所謂的執(zhí)行路徑?jīng)]有要求ln∈Final，n為路徑的長度. 在不需要強(qiáng)調(diào)動(dòng)作的情況下，路徑可以直接用狀態(tài)序列表示，例如l0l1…ln.

基于Σ，下面給出前綴閉合字串集的概念.令Σ+表示Σ中元素構(gòu)成的所有字串的集合，不包含空串.

定義2. 令ws?Σ+，如果對(duì)于任意str∈ws，str的任意非空串的前綴pre滿足pre∈ws，則ws被稱為前綴閉合字串集.

令PathG?Σ+為CFG G=〈Σ,Start,Act,→,Final〉的所有路徑的集合，根據(jù)定義2可知PathG為前綴閉合字串集合. 對(duì)于某程序的控制流模型G，狀態(tài)集合Σ是有限集合，但由于循環(huán)結(jié)構(gòu)的存在，PathG可以是無限的. 路徑集合PathG是根據(jù)G(程序)的靜態(tài)結(jié)構(gòu)所得到的,沒有考慮程序的語義,因此包含程序任意可能的執(zhí)行路徑.程序中的任意循環(huán)結(jié)構(gòu)都假定循環(huán)體能執(zhí)行任意次，即使循環(huán)次數(shù)為定值的循環(huán)結(jié)構(gòu)，換句話說，在計(jì)算PathG時(shí)，對(duì)循環(huán)條件不做任何解釋，條件true，n≤10和x2+y3≠a4+b5在任何環(huán)境里，具有一樣的效果，僅是一個(gè)未解釋的循環(huán)條件.p,p′∈PathG，當(dāng)p為p′的前綴時(shí)可記為pp′，顯然結(jié)構(gòu)〈PathG,〉為偏序集.

為了討論問題需要，下面給出函數(shù)last和函數(shù)MinPathG的說明.函數(shù)last:PathG→Σ用于計(jì)算給定路徑的終止?fàn)顟B(tài)，即last(l0l1…ln)=ln，last是部分函數(shù)，如果p∈PathG是無限路徑，last(p)沒有定義.MinPathG:Σ→(PathG)為給定狀態(tài)的最短路徑計(jì)算函數(shù)，(PathG)表示PathG的冪集，當(dāng)狀態(tài)l∈Σ和路徑S?PathG滿足以下條件1和條件2時(shí)，MinPathG(l)=S：1)對(duì)于s∈S，last(s)=l；2)對(duì)于s∈S，當(dāng)s′s，last(s′)≠l.路徑之間的偏序關(guān)系可擴(kuò)展至路徑集合的情形，給定l,l′∈Σ，MinPathG(l)MinPathG(l′)等價(jià)于?p∈MinPathG(l)·?p′∈MinPathG(l′)·pp′.

定義3. 〈Σ,?〉.令G=〈Σ,Start,Act,→,Final〉，??Σ×Σ：

1) 對(duì)于任意的l1,l2∈Σ，如果MinPathG(l1)MinPathG(l2)，那么l1?l2；

2) 假如存在路徑集合P=l0l1…li(li+1|ii+2|li+2|ii+3…|li+j)*li+j+1?PathG，并且li+j+1≠li+1,li+j+1≠li+2,…,li+j+1≠li+j，則li+1?li+j+1，li+2?li+j+1，…，li+j?li+j+1.

在定義3中，P=l0l1…li(li+1|ii+2|li+2|ii+3|…|li+j)*li+j+1使用了正規(guī)式語言的描述方法，式中|和*運(yùn)算代表“或”運(yùn)算和“閉包”運(yùn)算.根據(jù)正規(guī)式語言的解釋，正規(guī)式實(shí)質(zhì)上描述的是語言，即字串(路徑)的集合.閉包運(yùn)算用于描述程序中循環(huán)結(jié)構(gòu)的控制流模型，代表循環(huán)體執(zhí)行任意次，包括0次.圖2(a)給出了圖1所示程序的控制流模型，根據(jù)定義3可知〈{l0,l1,…,l18},?〉是嚴(yán)格偏序集.實(shí)質(zhì)上〈Σ,?〉反映了相關(guān)CFG的拓?fù)浣Y(jié)構(gòu)所關(guān)聯(lián)程序的控制結(jié)構(gòu)信息及程序執(zhí)行語義信息,但并不是根據(jù)任意的CFG構(gòu)造出的結(jié)構(gòu)〈Σ,?〉都是完備格.圖2(b)所示的CFG由于存在goto動(dòng)作(goto相當(dāng)于Act中的assume(true))，并進(jìn)行了特殊的無條件跳轉(zhuǎn)，導(dǎo)致該CFG相關(guān)的〈Σ,?〉為非偏序集結(jié)構(gòu).從圖2(b)可以看出，該CFG存在路徑集合P1=l0l1(l2l4l5)*l8l3l6l7和P2=l0l1l3l6l9l5l4(l2l4l5)*l8l3，根據(jù)?的定義，從P1和P2分別可以得出以下的關(guān)系式：l6?l2，l6?l4，l6?l5和l6?l2,l6?l4,l6?l5，顯然〈Σ,?〉不是偏序集.當(dāng)然，并不是所有含有g(shù)oto動(dòng)作的CFG相關(guān)的〈Σ,?〉都不是偏序集.實(shí)質(zhì)上圖2(a)中的assume(true)也是一種無條件轉(zhuǎn)移操作，相當(dāng)于goto的作用，但由于assume(true)轉(zhuǎn)移的目標(biāo)狀態(tài)受到限制，例如僅僅限于循環(huán)的開始狀態(tài)，不影響關(guān)系?的結(jié)構(gòu).另外，結(jié)合動(dòng)作assume(c)，其中c不為false和true，assume(true)能實(shí)現(xiàn)大多數(shù)高級(jí)程序設(shè)計(jì)語言循環(huán)結(jié)構(gòu)經(jīng)常使用的“break”和“continue”語句的功能，根據(jù)關(guān)系的定義，CFG中這種類型的assume(true)動(dòng)作不影響?的結(jié)構(gòu).

Fig. 2　The CFG examples.圖2　CFG實(shí)例

從B?hm-Jacopini定理[26-27]可知，CFG能表達(dá)由順序結(jié)構(gòu)、選擇結(jié)構(gòu)和循環(huán)結(jié)構(gòu)構(gòu)成的可計(jì)算函數(shù)，并且含有“goto”語句的可計(jì)算函數(shù)可通過算法等價(jià)轉(zhuǎn)換為不含“goto”、由3種結(jié)構(gòu)構(gòu)成的函數(shù).根據(jù)程序語言理論，對(duì)于描述程序的CFG，當(dāng)assume(true)∈Act的作用僅限于循環(huán)結(jié)構(gòu)的無條件轉(zhuǎn)換、“break”和“continue”時(shí)，如果l,l′∈Σ滿足l?…?l′，則l′?…?l.本文把描述不含有“goto”語句的程序的CFG稱為受限CFG，后文沒有特別說明，所涉及的CFG都局限于這種類型.

定理1. G=〈Σ,init,Act,→,final〉為不含“goto”語句的可計(jì)算函數(shù)構(gòu)造的CFG，〈Σ,?〉為嚴(yán)格偏序結(jié)構(gòu).

證明. 該定理的證明可基于程序的靜態(tài)結(jié)構(gòu)進(jìn)行歸納證明，下面對(duì)證明過程做出詳細(xì)的說明.可計(jì)算函數(shù)由順序結(jié)構(gòu)、選擇結(jié)構(gòu)和循環(huán)結(jié)構(gòu)組成，這些結(jié)構(gòu)從單純的基礎(chǔ)結(jié)構(gòu)，通過嵌套構(gòu)成任意復(fù)雜的結(jié)構(gòu).這3種結(jié)構(gòu)分別用seq，branch，loop表示，不同的同種結(jié)構(gòu)可用下標(biāo)進(jìn)行區(qū)分，seq(str1,str2,…,strn) 表示由結(jié)構(gòu)str1，str2,…,strn順序組成的順序結(jié)構(gòu)，branch(c,str1,str2)是選擇條件為c且真分支和假分支結(jié)構(gòu)分別為str1和str2的選擇結(jié)構(gòu)，branch(c,str)表示只有真分支的選擇結(jié)構(gòu)，loop(c,str)是循環(huán)條件為c、循環(huán)體為str的循環(huán)結(jié)構(gòu)，顯然，可計(jì)算函數(shù)也可表示為多層嵌套的3種結(jié)構(gòu)之一.因此只要說明每種結(jié)構(gòu)所涉及的狀態(tài)集與關(guān)系?構(gòu)成偏序集即可.令Σ[str]表示結(jié)構(gòu)str所涉及的狀態(tài)集，根據(jù)程序語言理論，當(dāng)str1和str2沒有嵌套關(guān)系時(shí)，Σ[str1]∩Σ[str2]=?.

1) 基礎(chǔ)步.當(dāng)str，str1，str2為基本順序結(jié)構(gòu)時(shí)，branch(c,str1,str2)和loop(c,str)分別為基本選擇結(jié)構(gòu)和基本循環(huán)結(jié)構(gòu). 顯然〈Σ[str],?〉為線性偏序集，〈{lc}∪Σ[str1],?〉，〈{lc}∪Σ[str2],?〉，〈{lc}∪Σ[str],?〉分別為線偏序集，因此〈{lc}∪Σ[str1]∪Σ[str2],?〉為偏序集，即〈Σ[branch(c,str1,str2)],?〉為偏序集.并且這些偏序集都存在最小元素，結(jié)構(gòu)str如果存在最小元素，則記為min(str).lc為選擇或循環(huán)結(jié)構(gòu)的入口狀態(tài).

2) 假設(shè)步和歸納步.假設(shè)〈Σ[str1],?〉,〈Σ[str2], ?〉,…,〈Σ[strn],?〉都為偏序集，且str1,str2, …,strn都存在最小元素.下面說明〈Σ[seq(str1,str2,…,strn)], ?〉為偏序集.根據(jù)順序結(jié)構(gòu)的構(gòu)造原理，對(duì)于1≤i≤n-1，任意l∈Σ[stri]，l?min(stri+1)，所有〈Σ[stri]∪Σ[stri+1],?〉為偏序集，且有最小元min(stri).因此〈Σ[str1]∪Σ[str2]∪…∪Σ[strn],?〉為偏序集，最小元為min(str1)，即〈Σ[seq(str1,str2,…,strn)],?〉為偏序集，且min(seq(str1,str2,…,strn))=min(str1).采用類似的方法，容易證明〈Σ[branch(c,str1,str2)],?〉和〈Σ[loop(c,str1)],?〉分別為偏序集并且存在最小元lc.

證畢.

定義4. 令G=〈Σ,init,Act,→,final〉，〈Σ,?〉是偏序集，函數(shù)rankG:Σ→滿足以下性質(zhì)時(shí)，稱為CFG G的位階函數(shù)：

1) 對(duì)于任意的l1,l2∈Σ，如果l1?l2，rankG(l1)

2)rankG是一一映射函數(shù)，即對(duì)于任意l≠l′，rankG(l)≠rankG(l′).

圖2(a)所示的CFG相關(guān)的位階函數(shù)rankG(li)=i+1，其中0≤i≤18，狀態(tài)值及相應(yīng)位階函數(shù)值標(biāo)記在相應(yīng)的狀態(tài)里.位階函數(shù)作為一種特殊的函數(shù)，把程序的控制結(jié)構(gòu)信息及程序執(zhí)行語義信息與自然數(shù)集進(jìn)行關(guān)聯(lián)，用于解釋CFITL公式的區(qū)間信息.位階函數(shù)是由〈Σ,?〉誘導(dǎo)的，且映射結(jié)果在<上保序，如果CFG相關(guān)的〈Σ,?〉不為偏序集，這意味著該CFG不能定義相應(yīng)的位階函數(shù)；但如果位階函數(shù)存在的話，則位階函數(shù)不是唯一的.例如：任意n≥1，rankG(li)=n×(i+1)都是圖2(a)所示CFG的位階函數(shù).圖2(b)所示的CFG由于存在goto動(dòng)作，進(jìn)行了特殊的無條件跳轉(zhuǎn)，導(dǎo)致該CFG的拓?fù)浣Y(jié)構(gòu)沒有相應(yīng)的位階函數(shù).

1.2.2CFITL的解釋模型

其中，s[op]表示符號(hào)狀態(tài)s執(zhí)行動(dòng)作op∈Act的后繼狀態(tài)，[c]s表示基于符號(hào)狀態(tài)s評(píng)估條件c的真假值，A[v←e]表示A′:Vars→Terms，對(duì)于v′∈Vars：當(dāng)v′≠v，A′(v′)=A(v′)；當(dāng)v′=v，A′(v′)=[e]s，[e]s與[c]s類似，表示在符號(hào)狀態(tài)s評(píng)估表達(dá)式e的值.對(duì)于符號(hào)狀態(tài)s，如果Π是不可滿足的，則表示s是不可達(dá)的，即程序的靜態(tài)結(jié)構(gòu)中存在死代碼.

根據(jù)符號(hào)狀態(tài)的變遷關(guān)系，執(zhí)行路徑p=l0l1…∈PathG可用符號(hào)狀態(tài)路徑s0s1…表示.其中s0=〈l0,A0,Π0〉為初始符號(hào)狀態(tài)，A0用符號(hào)變量或常量初值對(duì)所有的程序變量進(jìn)行初始化;Π0則記錄程序變量之間的約束關(guān)系，假如程序變量之間沒有任何約束，Π0=true.如果s0是唯一的，每條路徑p∈PathG對(duì)于唯一的符號(hào)狀態(tài)路徑.對(duì)于i≥0，〈li,op,li+1〉∈→，si+1=si[op].為了表達(dá)方便，令SP(p)為執(zhí)行路徑所對(duì)應(yīng)的符號(hào)狀態(tài)路徑，SG為G相關(guān)的符號(hào)狀態(tài)集合；Loc(s)=l，Eval(s)=A，Cond(s)=Π，其中s=〈l,A,Π〉.如果對(duì)出現(xiàn)在符號(hào)狀態(tài)中的符號(hào)變量用相應(yīng)類型的常量進(jìn)行代換得到DVars類型的程序變量值狀態(tài)及相應(yīng)的值狀態(tài)變遷路徑.令SV(s)表示出現(xiàn)在符號(hào)狀態(tài)s里的符號(hào)變量，DSV(s)同DVars意義類似，表示符號(hào)變量值域的笛卡兒積，E(s)=SV(s)→DSV(s)為對(duì)符號(hào)變量進(jìn)行常量賦值的映射集合，被稱為符號(hào)狀態(tài)s的環(huán)境.一般情況下，集合Act中的動(dòng)作不會(huì)引進(jìn)新的符號(hào)變量，因此任何符號(hào)狀態(tài)路徑中的符號(hào)變量集合為SV(s0)，所有符號(hào)狀態(tài)s的環(huán)境滿足E(s)?E(s0).對(duì)任意環(huán)境E，記E(Π)={A∈E|E(E0(Cond(s))∧Loc(s)=l)，其中E0=E(s0)，l∈Σ，s∈SG.

定義5. 給定CFG G=〈Σ,init,Act,→,final〉和rankG，二元組M=〈G,rankG〉稱為含序CFG結(jié)構(gòu). 下面基于含序CFG結(jié)構(gòu)M及符號(hào)狀態(tài)路徑建立區(qū)間時(shí)序邏輯CFITL的解釋模型.(M,l0)Eψ表示在環(huán)境E下結(jié)構(gòu)M的狀態(tài)l0滿足公式ψ，具體定義如下：

(M,l0)Etrue iff E≠?.

(M,l0)Epiff ?s=〈l0,A0,Π0〉∈SG·?A∈E(Π0)·A0∧Ap.

(M,l0)Eψ1∧ψ2iff (M,l0)Eψ1and (M,l0)Eψ2.

(M,l0)Eψ1∨ψ2iff ?s=〈l0,A0,Π0〉∈SG·?A∈E·((M,l0){A}ψ1∨(M,l0){A}ψ2).

(M,l0)Eψiff (M,l0)Eψ.

(M,l0)Eψiff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧(M,l1)E (Cond(s1))ψ).

(M,l0)Eψiff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧(M,l1)E (Cond(s1))ψ).

(M,l0)Eψiff ?P=l0l1…l∞∈PathG·(SP(P)=s0s1…∧?i≥0·(M,Loc(si))E (Cond(si))ψ).

(M,l0)Eψiff ?P=l0l1…l∞∈PathG·(SP(P)=s0s1…∧?i≥0·(M,Loc(si))E (Cond(si))ψ).

(M,l0)Eψiff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?i≥0·(M,Loc(si))E (Cond(si))ψ).

(M,l0)Eψiff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?i≥0·(M,Loc(si))E (Cond(si))ψ).

(M,l0)E(ψ1ψ2) iff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?j≥0·(?0≤i

(M,l0)E(ψ1ψ2) iff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?j≥0·(?0≤i

(M,l0)EIψiff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?i≥0·(rankG(li)∈I∧(M,li)

(M,l0)EIψiff ?=l0l1…∈PathG·(SP(P)=s0s1…∧?i≥0·(rankG(li)∈I∧(M,li)

(M,l0)EIψiff ?P=l0l1…l∞∈PathG·(SP(P)=s0s1…∧?i≥0·(rankG(li)∈I∧(M,li)

(M,l0)EIψiff ?P=l0l1…l∞∈PathG·(SP(P)=s0s1…∧?i≥0·(rankG(li)∈I→(M,li)

(M,l0)E(ψ1Iψ2) iff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?j≥0·(rankG(lj)∈I∧(M,lj)

(M,l0)E(ψ1Iψ2) iff ?P=l0l1…∈PathG·(SP(P)=s0s1…∧?j≥0·(rankG(lj)∈I∧(M,lj)

關(guān)于CFITL語義模型的解釋，做出如下進(jìn)一步的4點(diǎn)說明：

1) 語義定義中p∈AP，P=l0l1…l∞表示2種類型的路徑：無限路徑或滿足l∞=final的有限路徑.當(dāng)P為無限路徑時(shí)，l∞不表示具體的狀態(tài)，只是表達(dá)無限的概念.標(biāo)準(zhǔn)的CTL語義解釋是基于無限路徑的，路徑只與系統(tǒng)的動(dòng)態(tài)行為相關(guān)；CFITL的語義解釋是基于符號(hào)狀態(tài)路徑，既可能為無限路徑，也可能為有限路徑，并且符號(hào)狀態(tài)路徑集成了系統(tǒng)動(dòng)態(tài)行為信息及程序靜態(tài)結(jié)構(gòu)信息.

2) 當(dāng)環(huán)境E=?，對(duì)于任意ψ，(M,l)Eψ.當(dāng)l0=init時(shí)，(M,l0)Eψ可簡寫為(M,l0)ψ，此時(shí)環(huán)境為初始環(huán)境，即E(s0)；當(dāng)l0≠init時(shí)，由于從初始狀態(tài)init開始，可能存在多條路徑到達(dá)l0，根據(jù)定義5可知，每條路徑可以產(chǎn)生環(huán)境映射，因此(M,l0)ψ意味著對(duì)于所有可能的環(huán)境E而言，(M,l0)Eψ成立.利用當(dāng)E=?，(M,l)E true的性質(zhì)，可通過檢驗(yàn)(M,init)true是否成立來判斷程序是否存在死代碼.當(dāng)該屬性不成立，說明存在死代碼.

3) 由于CFITL的語義模型與CTL語義模型有著根本的差異，因此一些在CTL里很自然的、符合直覺的邏輯關(guān)系在CFITL里不一定成立，例如ψ?ψ，ψ?ψ，如果(M,l0)Eψ1∨ψ2并不等價(jià)于(M,l1)Eψ1∨(M,l0)Eψ2等.

4) 集合Act含有2種類型的動(dòng)作：賦值動(dòng)作v=e和條件判定動(dòng)作assume(c).在程序語言層面，賦值動(dòng)作改變程序變量的值，程序的執(zhí)行語義模型的狀態(tài)遷移描述了這種遷移前后狀態(tài)之間的關(guān)系；條件判定動(dòng)作不會(huì)改變程序變量的值，一般隱式或顯式地作為前一種動(dòng)作的約束條件體現(xiàn)在程序的語義模型的狀態(tài)變遷中.用于解釋CFITL公式中時(shí)序算子的路徑l0l1…包含2種操作所導(dǎo)致的CFG結(jié)構(gòu)中的狀態(tài)變遷，這種時(shí)序的觀念集成了程序靜態(tài)結(jié)構(gòu)的“序”概念和體現(xiàn)程序動(dòng)態(tài)行為的程序變量值狀態(tài)變化的“序”概念，這一點(diǎn)與CTL公式時(shí)序算子的“序”的解釋不一樣.當(dāng)然，通過簡單的轉(zhuǎn)換，可以去掉路徑l0l1…中操作assume(c)所導(dǎo)致的狀態(tài)變遷，建立起與CTL標(biāo)準(zhǔn)解釋模型Kripke結(jié)構(gòu)一致的“序”的觀念.

按照CFITL公式的語義解釋，下面分別用CFITL公式描述圖1所示程序應(yīng)該滿足的4條典型性質(zhì)：

以上的公式中，delete(b)表示命題“數(shù)組b所占用的內(nèi)存空間被釋放”，Zero(a)表示命題“數(shù)組a所有的元素值為0”，Zero(a,0,spot)表示命題“數(shù)組a從第1個(gè)元素至第spot個(gè)元素的值為0”.性質(zhì)2中2個(gè)公式等價(jià)，描述的是同一性質(zhì)，19是[19,19]的簡寫.根據(jù)公式的語義解釋可知，圖1所示程序滿足性質(zhì)2～4，不滿足性質(zhì)1.

1.2.1節(jié)論及對(duì)于給定的CFGG，如果存在位階函數(shù)，則存在無窮個(gè)滿足定義4的位階函數(shù).這意味著同一描述程序結(jié)構(gòu)特征和動(dòng)態(tài)行為特征的CFITL公式可以構(gòu)造不同的含序CFG結(jié)構(gòu)〈G,rankG〉，對(duì)公式給出不同的解釋.為了消除CFITL公式相對(duì)于CFG所呈現(xiàn)的多義性，下面提出規(guī)范化位階函數(shù)的概念.正如定理1的證明所述，一個(gè)可計(jì)算函數(shù)(程序)是由順序結(jié)構(gòu)、選擇結(jié)構(gòu)及循環(huán)結(jié)構(gòu)3種類型的程序塊通過嵌套的方式所產(chǎn)生，并且程序本身也屬于這3種結(jié)構(gòu)之一.為了表述方便，引進(jìn)表達(dá)式P[str1,str2,…,strn]，其中P,str1,str2,…,strn是seq,branch或loop類型的結(jié)構(gòu).P[str1,str2,…,strn]結(jié)構(gòu)表示程序P包含n個(gè)各種結(jié)構(gòu)的程序塊str1,str2,…,strn，表達(dá)式中的逗號(hào)“,”與seq(str1,str2,…,strn)或branch(c,str1,str2)中的逗號(hào)不一樣，沒有“序”的概念.任意2個(gè)不同的程序塊Bi和Bj可以是嵌套關(guān)系或非嵌套關(guān)系.G=〈Σ,init,Act,final,→〉為與P相關(guān)的CFG；rankG為G的某個(gè)位階函數(shù)，如果rankG滿足下列4個(gè)條件，則被稱為規(guī)范化位階函數(shù)(規(guī)范化位階函數(shù)記為nrankG)：

1) 對(duì)于任意l∈Σ，1≤rankG(l)≤|Σ|，即函數(shù)rankG為類型Σ→[1,|Σ|]的雙射函數(shù).

2) 對(duì)于P的任意程序塊Bi，當(dāng)l∈Σ[stri]，rankG(l)∈[low,high]，對(duì)于任意n∈[low,high]，存在l∈Σ[stri]，rankG(l)=n.顯然1≤low≤high≤|Σ|.滿足此條件的位階函數(shù)確保屬于同一程序塊的狀態(tài)集合所對(duì)應(yīng)的序數(shù)集合為某一完整的自然數(shù)區(qū)間.

3) 當(dāng)stri為選擇結(jié)構(gòu)程序塊，strt和strf分別為“真”分支程序塊和“假”分支程序塊，則對(duì)于任意l∈Σ[strt]，l′∈Σ[strf]，rankG(l)

4) 對(duì)于任意基本程序塊stri和strj，如果它們之間沒有嵌套關(guān)系，并且rankG(Σ[stri])=[low1,high2]，rankG(Σ[strj])=[low2,high2],則[low1,high1]∩[low2,high2]=?，如果stri嵌套于strj，則Σ[stri]?Σ[strj]，式中rankG(Σ[str])={n∈|n=rankG(l),l∈Σ[str]}，str為任意結(jié)構(gòu)的程序塊.

對(duì)于給定的CFG G，如果〈Σ,?〉是偏序集，則存在位階函數(shù)rankG及相應(yīng)的規(guī)范化位階函數(shù)nrankG，且該規(guī)范化位階函數(shù)是唯一的.定理2給出了規(guī)范化位階函數(shù)存在性和唯一性的證明.如果用含序CFG結(jié)構(gòu)〈G,nrankG〉代替普通的含序CFG結(jié)構(gòu)〈G,rankG〉，則CFITL公式的解釋具有唯一性.下文如果沒有特別說明，CFITL公式的解釋都是基于規(guī)范化位階函數(shù).

給定程序P、該程序誘導(dǎo)的偏序集〈Σ,?〉、規(guī)范化位階函數(shù)nrankG、程序P所包含的結(jié)構(gòu)str，并且任意l∈Σ[str]，nrankG(l)∈[low,high].

結(jié)論1. 當(dāng)str為順序結(jié)構(gòu)seq(str1,str2,…,strn)，根據(jù)規(guī)范化位階函數(shù)的定義可得以下性質(zhì)：

2) 對(duì)于任意1≤i

結(jié)論2. 當(dāng)str為選擇結(jié)構(gòu)branch(c,strt,strf)，同理可得以下性質(zhì)：

1) |Σ[str]|=|Σ[strt]|+|Σ[strf]|+2=high-low+1，式中的2表示選擇結(jié)構(gòu)的開始狀態(tài)和結(jié)束狀態(tài)；

2)nrankG(lc)=low，nrankG(lend)=high，lc和lend分別為開始狀態(tài)和結(jié)束狀態(tài)；

3) 任意l∈Σ[strt]，nrankG∈[low+1,low+|Σ[strt]|]，l∈Σ[strf]，nrankG(l)∈[low+Σ[strt]+1,high-1].當(dāng)str為只有真分支的選擇結(jié)構(gòu)branch(c,strt)時(shí)，|Σ[str]|=|Σ[strt]|+1=high-low+1，任意l∈Σ[strt]，nrankG(l)∈[low+1,high]，nrankG(lc)=loc.

結(jié)論3. 當(dāng)str為循環(huán)結(jié)構(gòu)loop(c,str)，根據(jù)關(guān)系?的定義可知，循環(huán)結(jié)構(gòu)中具有無條件轉(zhuǎn)移作用，但轉(zhuǎn)移目標(biāo)狀態(tài)受限的動(dòng)作assume(c)對(duì)構(gòu)造?的拓?fù)浣Y(jié)構(gòu)沒有實(shí)質(zhì)性的影響，因此對(duì)于循環(huán)結(jié)構(gòu)loop(c,str)和選擇結(jié)構(gòu)loop(c,str)而言，規(guī)范化位階函數(shù)nrankG在狀態(tài)集合Σ[loop(c,str)]上的性質(zhì)是等價(jià)的.

定理2. 對(duì)于CFG G=〈Σ,init,Act,final,→〉，如果〈Σ,?〉為偏序結(jié)構(gòu)，則G存在規(guī)范化位階函數(shù)nrankG，且是唯一的.

證明. 如果〈Σ,?〉是偏序結(jié)構(gòu)，G顯然存在位階函數(shù).令P為與G相關(guān)的程序，不失一般性，設(shè)其結(jié)構(gòu)為seq(str1,str2,…,strn)，其中stri為順序結(jié)構(gòu)、選擇結(jié)構(gòu)或循環(huán)結(jié)構(gòu)，1≤i≤n.下面通過一個(gè)構(gòu)造性算法證明規(guī)范化位階函數(shù)的存在性和唯一性. G的位階函數(shù)rankG按以下2個(gè)步驟進(jìn)行構(gòu)造：

2) 假如Str_Vector≠?，從集合Str_Vector中選擇結(jié)構(gòu)str(Str_Vector=Str_Vector{str})：

① 假如str為不含有選擇或循環(huán)結(jié)構(gòu)的順序結(jié)構(gòu)，則l∈Σ[str]，nrankG(l)∈Istr，且在區(qū)間Istr，rankG具有保序的性質(zhì),Istr是結(jié)構(gòu)所屬的區(qū)間信息；

② 假如str為含有嵌套結(jié)構(gòu)的順序結(jié)構(gòu)、選擇結(jié)構(gòu)或循環(huán)結(jié)構(gòu)，則按照結(jié)論1～3的方法，把相關(guān)的內(nèi)嵌結(jié)構(gòu)加入str_Vector，并設(shè)置相關(guān)結(jié)構(gòu)所屬的區(qū)間，并返回步驟①.

顯然按照以上步驟構(gòu)造的rankG符合規(guī)范化位階函數(shù)的性質(zhì)要求,并且交換任意2個(gè)互相不嵌套結(jié)構(gòu)的區(qū)間，不滿足規(guī)范化位階函數(shù)的要求，即規(guī)范化位階函數(shù)是唯一的.

證畢.

2　模型檢驗(yàn)

2.1基于顯式狀態(tài)枚舉的CFITL模型檢驗(yàn)

第1節(jié)通過環(huán)境、符號(hào)狀態(tài)及符號(hào)狀態(tài)路徑對(duì)CFITL公式的語義進(jìn)行了詳細(xì)的定義，在此基礎(chǔ)上，本節(jié)重點(diǎn)討論基于CFITL的模型檢驗(yàn)方法.模型檢驗(yàn)的研究始于20世紀(jì)80年代[5]，主要用于驗(yàn)證有限狀態(tài)系統(tǒng)是否滿足一些特定的性質(zhì).基本思想是：用遷移系統(tǒng)表示系統(tǒng)的行為，用模態(tài)時(shí)序邏輯公式描述系統(tǒng)的性質(zhì)，系統(tǒng)是否滿足某個(gè)性質(zhì)就轉(zhuǎn)化為“遷移系統(tǒng)是否是相應(yīng)的模態(tài)邏輯公式的模型”這樣的數(shù)學(xué)問題.模型檢驗(yàn)的核心問題是設(shè)計(jì)可行的算法，自動(dòng)化檢驗(yàn)遷移系統(tǒng)是否是相應(yīng)的模態(tài)邏輯公式的模型.根據(jù)模態(tài)邏輯公式類型和表達(dá)能力以及不同的算法原理，可以構(gòu)造各種不同類型的算法用于完成模型檢驗(yàn)問題的求解.盡管這些算法類型各異，但根本上它們?cè)趫?zhí)行同一任務(wù)：可達(dá)狀態(tài)空間的計(jì)算.

DnrankG×DVars·(?t=〈l,op,l′〉∈→·

算法1. 模型檢驗(yàn)算法CheckEG(f).

輸入：公式f、程序P；

輸出：可達(dá)狀態(tài)集合S.

④S=SSCC;

⑤ while (SSCC≠?) do

⑦SSCC=SSCC

算法2. 模型檢驗(yàn)算法CheckEU(I,f1,f2).

輸入：公式f1、公式f2、區(qū)間I；

輸出：可達(dá)狀態(tài)集合S.

②S=S;

③ while (S≠?) do

⑤S=S

⑨ end while

算法3. 路徑測試函數(shù)TestSymPath(S,sp).

輸入：S,sp；

① if (sp=l0l1…ln為符號(hào)化路徑，ln為終止?fàn)顟B(tài))

②SymS={si‖0≤i≤n,SP(sp)=s0s1…sn};

③ while (SymS≠?)

④chooses=〈l,A,Π〉∈SymS;

⑤SymS=SymS{s};

?A∈E(s)·(val=A[A])};

⑧ end while

⑨ return success;

函數(shù)TestSymPath中參數(shù)S表示值狀態(tài)集合，例如算法1中的S，sp為待測試符號(hào)路徑，可以采用正規(guī)語言的方式表達(dá).參數(shù)kmax是與SCC相關(guān)的一個(gè)參數(shù)，是反映SCC路徑模式的一個(gè)參數(shù)，需要計(jì)算值狀態(tài)路徑與正規(guī)式表達(dá)的符號(hào)路徑模式匹配問題，需要很大的計(jì)算開銷. 如果在系統(tǒng)的有界模型檢驗(yàn)中存在閾值，則可取閾值作為kmax的保守值.當(dāng)狀態(tài)空間規(guī)模較小時(shí)，可采用模擬執(zhí)行計(jì)算符號(hào)路徑sp值狀態(tài)集合不動(dòng)點(diǎn)的方法進(jìn)行計(jì)算.

下面通過與CTL的對(duì)比討論CFITL模型檢驗(yàn)的算法復(fù)雜度.當(dāng)語義模型Kripke結(jié)構(gòu)〈S,R,L〉的狀態(tài)集S為有限時(shí)，CTL公式可滿足性是可判定的，算法復(fù)雜度為O(len(f)(Card(S)+Card(R))).當(dāng)系統(tǒng)實(shí)現(xiàn)的模型CFG所誘導(dǎo)的Kripke結(jié)構(gòu)為有限結(jié)構(gòu)時(shí)，由于刻畫有序CFG拓?fù)浣Y(jié)構(gòu)的數(shù)值特征為整數(shù)區(qū)間，狀態(tài)的數(shù)值屬性為單點(diǎn)型的區(qū)間，在此條件下，CFITL公式可滿足性是可判定的.本節(jié)基于擴(kuò)展后的狀態(tài)空間DnrankG×DVars構(gòu)造了部分公式的判定算法，算法的復(fù)雜度為O(len(f)(Card(DnrankG×DVars)+Card(R))).

CFITL模型檢驗(yàn)算法的復(fù)雜度較CTL模型檢驗(yàn)算法高，但并不是指數(shù)級(jí)的升高，受DnrankG約束.對(duì)于大狀態(tài)空間或無限狀態(tài)空間系統(tǒng)的模型檢驗(yàn)，傳統(tǒng)的基于抽象技術(shù)，例如謂詞抽象，經(jīng)過重新設(shè)計(jì)后仍然可以應(yīng)用于CFITL模型檢驗(yàn)，以緩解狀態(tài)空間爆炸問題；另外2.2節(jié)結(jié)合CFITL公式重寫技術(shù)的有界模型檢驗(yàn)也是一種實(shí)施途徑，這也是原型系統(tǒng)采用的基本方法.

2.2基于SMT的CFITL有界模型檢驗(yàn)

基于狀態(tài)枚舉的模型檢驗(yàn)算法一個(gè)首要的前提是構(gòu)建系統(tǒng)的有限狀態(tài)系統(tǒng)，例如算法1和算法2都只能應(yīng)用于有限狀態(tài)系統(tǒng).現(xiàn)實(shí)中的各種類型程序涉及復(fù)雜的邏輯控制及具有無限值域的抽象數(shù)據(jù)類型，不能直接獲得有限狀態(tài)的系統(tǒng)結(jié)構(gòu)，即使應(yīng)用各種類型的抽象建模技術(shù)[28-29]，但由于難以建立統(tǒng)一的、自動(dòng)化的抽象機(jī)制及抽象精化方法，各種抽象技術(shù)也只能緩解，而不能從根本上克服各種模型檢驗(yàn)方法所面臨的可控規(guī)模狀態(tài)空間的系統(tǒng)模型的構(gòu)建問題，包括符號(hào)模型檢驗(yàn)方法.另一方面，模型檢驗(yàn)方法的完備性是相對(duì)于系統(tǒng)規(guī)約而言的，但開發(fā)人員不可能給出完全正確且完備的系統(tǒng)規(guī)約，以確保所開發(fā)的目標(biāo)系統(tǒng)是完全“正確”的系統(tǒng)，而且，在資源受限的情況下，再先進(jìn)的模型檢驗(yàn)器也不可能對(duì)系統(tǒng)所有的屬性進(jìn)行驗(yàn)證.

基于以上這些因素，Clarke等人提出有界模型檢驗(yàn)的思想[9]，這種方法不要求驗(yàn)證具有完備性，并且把基于可達(dá)狀態(tài)集合的計(jì)算問題轉(zhuǎn)化為命題邏輯的可滿足性判定問題.這樣，模型檢驗(yàn)問題可以利用許多高效的可滿足性判定器求解，例如GRASP，SATO，ZCHAFF等[30-31]，從而避免可達(dá)狀態(tài)集計(jì)算所帶來的存儲(chǔ)空間和計(jì)算時(shí)間的開銷問題.從某種意義上，可以認(rèn)為有界模型檢驗(yàn)方法是介于測試和一般模型檢驗(yàn)之間的一種方法，它采用定理證明的方法測試在系統(tǒng)的局部行為空間內(nèi)規(guī)約是否成立，兼具測試和證明的特點(diǎn)，因此有界模型檢驗(yàn)除了用于證明屬性是否成立外，還經(jīng)常用于查找程序的錯(cuò)誤.

從上面的論述可以看出，有界模型檢驗(yàn)方法的性能和能力取決于可滿足性判定器.由于現(xiàn)代程序含有各種復(fù)雜的抽象數(shù)據(jù)類型及操作，包括GRASP和SATO等傳統(tǒng)的命題邏輯可滿足性判定器難以直接應(yīng)用于程序?qū)傩则?yàn)證.近年來，可滿足性模理論及相關(guān)工具得到了快速地發(fā)展，例如：Z3[32]，CVC，MathSAT等.SMT問題是命題邏輯公式可滿足性判定問題的擴(kuò)展：謂詞邏輯公式的可滿足性判定[25].純邏輯領(lǐng)域不涉及任何領(lǐng)域性的理論，但在實(shí)際的應(yīng)用中，大部分SMT判定器都內(nèi)建有復(fù)雜的領(lǐng)域理論，包括整數(shù)理論、實(shí)數(shù)理論、未解釋函數(shù)理論及一些處理復(fù)雜數(shù)據(jù)類型的理論，如向量、隊(duì)列和數(shù)組理論等. 這些背景理論的集成使得SMT判定器具有描述及推理復(fù)雜的特定領(lǐng)域問題的能力.許多程序分析與驗(yàn)證領(lǐng)域的問題：可驗(yàn)證的編譯方法、謂詞抽象、模型檢驗(yàn)等，這些問題都可轉(zhuǎn)化為SMT問題，利用集成多種不同背景理論的SMT判定器進(jìn)行求解.SMT研究領(lǐng)域的眾多的研究機(jī)構(gòu)和研究人員提出了SMT工具的標(biāo)準(zhǔn)通訊語言和命令，被稱為SMT-LIB，通過SMT-LIB可以方便地描述背景理論、各種復(fù)雜的待求解的問題及操縱各種SMT工具，并且這些SMT工具大都提供了豐富的人機(jī)接口和編程接口.

基于SMT的CFITL模型檢驗(yàn)方法的關(guān)鍵環(huán)節(jié)是把有界模型檢驗(yàn)問題歸結(jié)于SMT，用集成了各種域理論的謂詞邏輯語言進(jìn)行描述.給定含序CFG結(jié)構(gòu)M=〈G,nrankG〉，待驗(yàn)證時(shí)序?qū)傩詅及界限K(K≥0)，用[M,f]K表示長度為K的符號(hào)狀態(tài)路徑滿足f的充分必要條件， [M,f]K由2部分組成：1)長度為K的來自CFG G的符號(hào)狀態(tài)路徑的行為及靜態(tài)結(jié)構(gòu)規(guī)范，記為[M]K；2)滿足屬性f且長度為K的路徑應(yīng)該滿足的條件，記為[f]K，[M,f]K=[M]K∧[f]K.

由于符號(hào)狀態(tài)路徑s0s1…的最大長度為K，因此上式中i≤K-1，[p]si表示基于符號(hào)狀態(tài)si對(duì)命題p進(jìn)行解釋.根據(jù)語義定義可知，析取運(yùn)算∨的行為不具有一般意義上的那種直覺的性質(zhì)，即(M,l)Eψ1∨ψ2等價(jià)于(M,l)Eψ1∨(M,l)Eψ2，上式中關(guān)于析取運(yùn)算給出了一種更強(qiáng)的重寫結(jié)果，如果要得到等價(jià)SMT的編碼形式，則需要引入量詞.關(guān)于時(shí)序算子的重寫規(guī)則需要特別的進(jìn)一步的解釋.根據(jù)定義5可知，I和語義解釋涉及2種類型的符號(hào)狀態(tài)路徑：一種是無限路徑；一種是有限長度路徑，且當(dāng)程序執(zhí)行完該路徑后處于終止?fàn)顟B(tài).當(dāng)sK滿足Loc(sK)=final，且不存在op∈Act,l∈Σ，〈Loc(sK),op,l〉∈→時(shí)，即s0s1…sK是程序的一條完整的執(zhí)行路徑，則只要迭代應(yīng)用公式重寫規(guī)則計(jì)算出[和.當(dāng)s0s1…sK不是程序的完整路徑，即Loc(sK)≠final，或者當(dāng)Loc(sK)=final，存在op∈Act,l∈Σ，〈Loc(sK),op,l〉∈→，那么可以分成以下2種情況：

1) 當(dāng)該路徑為套索路徑(lasso-shape path)[33]時(shí)，有限路徑展現(xiàn)出無限路徑的性質(zhì)，該有限路徑滿足[或意味著相關(guān)的無限路徑滿足ψ或Iψ.當(dāng)存在0≤i≤K，并且存在op∈Act，〈Loc(sK),op,Loc(si)〉∈→，對(duì)于所有的A∈E(sK)，Eval(si)=Eval(sK)[op]，s0s1…si…sK為套索符號(hào)路徑，與其相關(guān)的無限路徑為sos1…(si…sK)ω,其中ω表示無限的意思.

上式中Δ表示任意的路徑量詞.需要強(qiáng)調(diào)的是上面所討論的在有界模型檢驗(yàn)的條件下證明ψ和Iψ的方法可靠但并不完備，因?yàn)楫?dāng)程序所實(shí)現(xiàn)的系統(tǒng)為無限狀態(tài)系統(tǒng)時(shí)，存在不含套索的無限路徑滿足ψ或Iψ.以一個(gè)沒有上界的簡單計(jì)數(shù)器為例，該系統(tǒng)是無限狀態(tài)系統(tǒng)，顯然容易得到一個(gè)不存在套索路徑且滿足(count≥0)的系統(tǒng)實(shí)現(xiàn)，count為計(jì)數(shù)器變量.如果結(jié)合符號(hào)狀態(tài)路徑的結(jié)構(gòu)特性和時(shí)序算子的語義特性，同樣可以得出一些關(guān)于[和的更有意義的結(jié)論.例如：如果有界符號(hào)路徑s0s1…sK不滿足[ψ]K或[Iψ]K，并不能得出沒有以s0s1…sK為前綴的路徑滿足[ψ]K或[Iψ]K，但如果s0s1…sK滿足IE，則可以據(jù)此得到可靠且完備的結(jié)論，即s0s1…sKΔIψ?s0s1…sK…ΔIψ.

從上面的相關(guān)分析可以看出，雖然有界模型檢驗(yàn)方法不是完備的，但結(jié)合模型結(jié)構(gòu)的分析，可以得到可靠且完備的結(jié)果，這方面的工作可參考文獻(xiàn)[9].

實(shí)際上，在實(shí)施模型檢驗(yàn)時(shí)，根據(jù)不同類型的屬性f，可以采用不同的驗(yàn)證策略.例如對(duì)于安全性屬性(p1∧p2)，可以通過驗(yàn)證是否滿足((p1∧p2))的結(jié)果考察屬性(p1∧p2).假如滿足((p1∧p2))，則(p1∧p2)不成立，并且滿足((p1∧p2))的符號(hào)狀態(tài)路徑是反例，進(jìn)一步調(diào)用SMT工具獲得值狀態(tài)路徑，結(jié)合2種類型的路徑信息，可以更精確地對(duì)程序進(jìn)行調(diào)試，定位程序錯(cuò)誤；當(dāng)在界限為K的條件下，((p1∧p2))不成立，則進(jìn)一步根據(jù)系統(tǒng)的結(jié)構(gòu)特性，例如完備的界限閾值及相關(guān)的路徑特征屬性信息LC，TC，IE等作出判斷，決定下一步采取的策略.對(duì)于形如p的活性屬性同樣可以采取2種驗(yàn)證策略.

3　VerTPCFG模型檢驗(yàn)器

CFITL直接用于描述程序的各類與靜態(tài)結(jié)構(gòu)及動(dòng)態(tài)行為相關(guān)的時(shí)序?qū)傩裕瑸榱耸顾O(shè)計(jì)的模型檢驗(yàn)器系統(tǒng)開發(fā)成本盡可能低、運(yùn)行自動(dòng)化程度盡可能高、能處理的程序數(shù)據(jù)類型和結(jié)構(gòu)盡可能豐富，盡量復(fù)用已有的高性能的開源軟件工具，基于SMT的有界模型檢驗(yàn)方法實(shí)現(xiàn)了相關(guān)的原型工具. CFITL有界模型檢驗(yàn)器總體架構(gòu)如圖3所示:

Fig. 3　The framework of bounded model checker over CFITL.圖3　CFITL有界模型檢驗(yàn)器框架

Fig. 4　The prototype system of VerTPCFG.圖4　VerTPCFG原型系統(tǒng)平臺(tái)

圖3所給模型檢驗(yàn)器設(shè)計(jì)框架中的大部分內(nèi)容在第2節(jié)都有所涉及,下面就圖中標(biāo)有★的部分內(nèi)容作進(jìn)一步的介紹.為了增強(qiáng)驗(yàn)證工具的可擴(kuò)展性，在程序和CFG之間設(shè)計(jì)了一個(gè)中間語言層，使得CFG獨(dú)立于具體的程序設(shè)計(jì)語言.具體的程序至中間語言的翻譯由預(yù)處理過程“preprocess”負(fù)責(zé)處理，不同的程序語言對(duì)應(yīng)不同的預(yù)處理過程.當(dāng)然，為了得到有序的CFG結(jié)構(gòu)，預(yù)處理過程還需要對(duì)原程序的語法進(jìn)行有效性檢查及程序的等價(jià)轉(zhuǎn)換，這方面的主要內(nèi)容包括有副作用語句的等價(jià)變換和有害“goto”語句的消除.中間語言采用STG Format[34]，這種語言由IF規(guī)約語言子集改編而成，用于描述各種復(fù)雜的順序及并發(fā)反應(yīng)式系統(tǒng).目標(biāo)系統(tǒng)的程序設(shè)計(jì)與實(shí)現(xiàn)是一種具有創(chuàng)新性的工作，深刻地體現(xiàn)開發(fā)人員的主觀能動(dòng)性，對(duì)于同樣的功能需求，具有不同知識(shí)背景和思維能力的人所設(shè)計(jì)程序的靜態(tài)語法結(jié)構(gòu)差異極大，單條語句語法與語義可能存在極大的差別.面臨這種情況，在構(gòu)造CFITL的語義模型有序CFG結(jié)構(gòu)時(shí)有2種處理策略：1)允許動(dòng)作集合Act的元素具有“副作用”，與源程序的語句保持一致，這樣使得CFG基本結(jié)構(gòu)與源程序具有相同的靜態(tài)語法結(jié)構(gòu)；2)限制集合Act元素的復(fù)雜性，使得它在語法層面上具有“原子性”，這樣CFG靜態(tài)結(jié)構(gòu)與源程序的靜態(tài)結(jié)構(gòu)會(huì)存在某種程度的不一致性.

第1種處理方法的優(yōu)點(diǎn)是開發(fā)人員可以依據(jù)自己的程序?qū)崿F(xiàn)寫出要求滿足的屬性公式，但這種方法有著顯而易見的缺點(diǎn)，即系統(tǒng)的動(dòng)態(tài)行為(狀態(tài)空間及狀態(tài)變遷關(guān)系)與語句形態(tài)高度耦合，CFITL的“時(shí)序”的意義沒有統(tǒng)一的解釋；第2種方法保持了對(duì)動(dòng)態(tài)行為模型的認(rèn)識(shí)觀點(diǎn)，使得CFITL的“時(shí)序”具有統(tǒng)一的解釋，即一個(gè)在語法層面上不具有副作用的原子語句的執(zhí)行就意味著系統(tǒng)變換至下一時(shí)刻點(diǎn).但第2種方法也有不足，由于程序與相關(guān)的CFG在結(jié)構(gòu)上存在不一致的地方，因此在描述涉及與結(jié)構(gòu)相關(guān)的屬性時(shí)，需要利用“compute_nrank”處理過程輸出有序CFG結(jié)構(gòu)的詳細(xì)信息.圖3所示的方法采用一種折中的方法，即CFG的構(gòu)建按照第2種處理策略，但屬性描述所涉及的結(jié)構(gòu)因素(區(qū)間)按照源程序的結(jié)構(gòu)特征進(jìn)行解釋.這種處理方法的優(yōu)點(diǎn)是屬性的描述不需要完整的CFG信息，屬性的結(jié)構(gòu)要素與源程序保持一致，最符合開發(fā)人員的直覺認(rèn)知.這會(huì)產(chǎn)生一個(gè)關(guān)鍵性的問題需要處理：建立虛擬CFG(Act集合與源程序的語句保持一致)與CFITL有序CFG結(jié)構(gòu)之間的結(jié)構(gòu)映射關(guān)系，這是過程“Interval_map”的核心工作.輸入“Verifying Strategy”代表2.2節(jié)的驗(yàn)證策略.給定一個(gè)待驗(yàn)證的屬性，可以根據(jù)公式的類型和特點(diǎn)及界限參數(shù)K，選擇“證明驅(qū)動(dòng)”策略或“反例驅(qū)動(dòng)”策略，不同的策略意味著不同的〖f〗K輸出.

基于圖3的系統(tǒng)架構(gòu)，設(shè)計(jì)了VerTPCFG原型系統(tǒng)，圖4顯示了該原型系統(tǒng).目前，該系統(tǒng)還缺乏真正的前端，僅實(shí)現(xiàn)了基于STG Format語言的系統(tǒng)規(guī)約及其靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為屬性的分析和驗(yàn)證.基于原型工具VerTPCFG，選取汽車風(fēng)擋刮水控制器(windscreen wiper controller)、飲料銷售自動(dòng)機(jī)(beverage machiner)和電梯控制器(elevator controller)作為基本實(shí)驗(yàn)對(duì)象，這些實(shí)驗(yàn)對(duì)象用STG Format語言進(jìn)行描述.每個(gè)實(shí)驗(yàn)對(duì)象各設(shè)計(jì)了4條屬性，這些屬性基本都含有靜態(tài)結(jié)構(gòu)因素，例如循環(huán)不變式屬性，界限的值簡單地根據(jù)由系統(tǒng)描述所產(chǎn)生的CFG中最長路徑長度確定，實(shí)驗(yàn)中人為確定為路徑長度的3倍.這些屬性大都是安全性屬性，因此除明確給出了反例的屬性外，大部分屬性的驗(yàn)證結(jié)果是不完備，原型工具沒有計(jì)算LC,TC,IE.實(shí)驗(yàn)結(jié)果表明各條屬性都在30 s以內(nèi)得到證明，當(dāng)然這與所給的屬性公式的文本復(fù)雜度較低，不涉及復(fù)雜的時(shí)序算子的嵌套及K的取值相對(duì)較低等多種因素相關(guān).通過觀察驗(yàn)證過程，發(fā)現(xiàn)較多亟待解決的問題，例如：驗(yàn)證[t1,t2]ψ類的屬性時(shí)，容易給出平凡的路徑，例如該路徑所有狀態(tài)的位階不屬于區(qū)間[t1,t2]；驗(yàn)證[t1,t2]ψ類屬性時(shí)會(huì)出現(xiàn)大量無意義的路徑信息的計(jì)算.由于原型系統(tǒng)沒有實(shí)現(xiàn)復(fù)雜數(shù)據(jù)類型的處理，且缺乏完整前端處理過程，即實(shí)現(xiàn)有效的程序?qū)崿F(xiàn)語言到中間語言的翻譯，因此僅選取了幾個(gè)偏于控制類型的簡單例子.

4　相關(guān)工作

時(shí)序邏輯和基于時(shí)序邏輯的軟硬件系統(tǒng)的時(shí)序?qū)傩砸?guī)約及驗(yàn)證是形式化方法領(lǐng)域的重要研究內(nèi)容，鑒于CTL和LTL在表達(dá)能力、語法的易用性和判定算法的效率等方面所具有的平衡性，與之相關(guān)的邏輯理論、判定算法和數(shù)據(jù)結(jié)構(gòu)及工具軟件的開發(fā)和應(yīng)用等方面的研究工作已經(jīng)取得豐富的成果，并且這些成果已經(jīng)成功地服務(wù)于工業(yè)界[1-2,5,8-12].國內(nèi)唐稚松院士較早開展了關(guān)于時(shí)序邏輯理論方面的研究工作，提出了XYZE時(shí)序邏輯系統(tǒng)，該邏輯系統(tǒng)包括2個(gè)語言子集 XYZAE和XYZEE，分別用于描述程序的靜態(tài)語義和動(dòng)態(tài)行為語義的屬性規(guī)約[35-36].

CTL和LTL等這些時(shí)序邏輯僅能用于描述系統(tǒng)的動(dòng)態(tài)語義屬性.顯然，系統(tǒng)的動(dòng)態(tài)行為屬性由程序?qū)崿F(xiàn)的靜態(tài)結(jié)構(gòu)屬性決定，直接對(duì)實(shí)現(xiàn)的結(jié)構(gòu)語義屬性進(jìn)行規(guī)約和推理具有重要的意義，是確保系統(tǒng)動(dòng)態(tài)行為屬性正確性的基礎(chǔ).近年有多種邏輯被提出，用于處理程序?qū)崿F(xiàn)的各種重要語法要素，例如指針和數(shù)組等，典型的包括分離邏輯[37]、范圍邏輯[38]和動(dòng)態(tài)邏輯[39]等.分離邏輯和范圍邏輯用于含有指針程序的屬性分析；而動(dòng)態(tài)邏輯則引入了類似于時(shí)序算子的模態(tài)算子，用于規(guī)約和推理程序的動(dòng)態(tài)行為屬性.另外，陳意云教授研究團(tuán)隊(duì)提出了指針邏輯和形態(tài)圖邏輯系統(tǒng)[40-41]用于對(duì)指針及遞歸數(shù)據(jù)結(jié)構(gòu)的性質(zhì)進(jìn)行分析.

相比上面所提及的幾類邏輯系統(tǒng)，CFITL具有顯著的特點(diǎn)和優(yōu)勢.類似于CTL和LTL的時(shí)序邏輯系統(tǒng)，只具有規(guī)約和推理系統(tǒng)動(dòng)態(tài)執(zhí)行語義屬性的能力，而缺乏規(guī)約系統(tǒng)實(shí)現(xiàn)的靜態(tài)結(jié)構(gòu)語義.CFITL則具備在統(tǒng)一的框架內(nèi)規(guī)約和推理靜態(tài)結(jié)構(gòu)語義和動(dòng)態(tài)行為語義屬性的能力.CFITL的語法定義是基于CTL擴(kuò)充而來的，但語義定義具有很大的差異，兩者的表達(dá)能力具有相關(guān)性，又有很大的差異性.例如對(duì)于只含有全稱路徑量詞的CTL屬性，在CFITL邏輯框架內(nèi)能進(jìn)行等價(jià)地表達(dá)；對(duì)于含有路徑量詞的公式，沒有或不易構(gòu)造相應(yīng)的CFITL等價(jià)式，但CFITL有相應(yīng)的一種更強(qiáng)的表達(dá)，即對(duì)于CTL公式fctl、CFITL公式fcfitl，如果(M,l0)fcfitl，則(K,s0)fctl，其中K為系統(tǒng)實(shí)現(xiàn)M所誘導(dǎo)的Kripke結(jié)構(gòu)，fctl和fcfitl語法具有一定關(guān)聯(lián)性.當(dāng)然，即使把這種更強(qiáng)的關(guān)系視為等價(jià)關(guān)系，也并不意味著CFITL語言包含CTL.顯然，由于CFITL引進(jìn)了區(qū)間的概念，關(guān)于靜態(tài)結(jié)構(gòu)屬性的CFITL大部分描述在CTL框架里顯然不能等價(jià)地表達(dá).當(dāng)然CTL和CFITL語義解釋之間的關(guān)系，下一步的工作將進(jìn)行更加細(xì)致的研究.

分離邏輯和范圍邏輯這類型的邏輯是Hoare-Floyd公理系統(tǒng)的擴(kuò)展，用于推理具有指針類行為程序的屬性，由于構(gòu)造系統(tǒng)的目的與CFITL不一致，它們不具備系統(tǒng)化描述動(dòng)態(tài)時(shí)序?qū)傩院挽o態(tài)結(jié)構(gòu)屬性的能力.XYZE系統(tǒng)和動(dòng)態(tài)邏輯系統(tǒng)可以直接用于規(guī)約和推理程序的行為屬性，并且定義了類似的時(shí)序算子.相對(duì)CFITL而言，XYZE和動(dòng)態(tài)邏輯系統(tǒng)具有較為復(fù)雜的語法體系，尤其是XYZE系統(tǒng)，它包含2個(gè)語言子系統(tǒng)，且定義了各種不同的原語，用于表達(dá)各種復(fù)雜時(shí)序?qū)傩运枰臅r(shí)序、邏輯及程序結(jié)構(gòu)相關(guān)的概念，動(dòng)態(tài)邏輯系統(tǒng)基本不具備描述靜態(tài)結(jié)構(gòu)屬性的能力；CFITL通過引進(jìn)整數(shù)區(qū)間作為程序結(jié)構(gòu)因素的映射，使之具備對(duì)程序各種簡單和復(fù)雜的結(jié)構(gòu)屬性進(jìn)行規(guī)約的表達(dá)能力；另外CFITL通過繼承CTL的語法和語義框架，使得許多CTL模型檢驗(yàn)方法理論和算法思想可應(yīng)用于CFITL模型檢驗(yàn)領(lǐng)域.

區(qū)間時(shí)序邏輯包括一類具有數(shù)量約束指標(biāo)范疇的時(shí)序邏輯，這些各種不同形式的數(shù)量指標(biāo)大都用于復(fù)雜系統(tǒng)的性能屬性，例如概率約束指標(biāo)、數(shù)值獎(jiǎng)賞指標(biāo)、連續(xù)或離散時(shí)間約束指標(biāo)和時(shí)鐘約束等，這方面詳情請(qǐng)參閱有關(guān)文獻(xiàn)[3,7,14,18,42-44].這些各種不同類型具有數(shù)量約束指標(biāo)的時(shí)序邏輯的目標(biāo)顯然還是系統(tǒng)的動(dòng)態(tài)語義范疇，與CFITL的作用有著根本的差別.另外還有一類典型的區(qū)間時(shí)序邏輯，例如PITL[45]、Halpern-Shoham邏輯[46](簡稱HS邏輯)及國內(nèi)段振華教授提出的PTL[47]，它們的語義解釋是線性離散時(shí)間結(jié)構(gòu)，用于規(guī)約和推理具有離散時(shí)間刻度并發(fā)系統(tǒng)的離散時(shí)間相關(guān)的各類行為屬性.基于PITL，PTL通過引進(jìn)投影和投影星操作，使之具備規(guī)約和推理并發(fā)系統(tǒng)時(shí)間區(qū)間上的重復(fù)性屬性，甚至類似于公正性要求的無窮次重復(fù)的屬性以及進(jìn)程同步性屬性，文獻(xiàn)[48]進(jìn)一步把PTL用于單調(diào)速率調(diào)度算法可調(diào)度性的驗(yàn)證.基于不同的動(dòng)機(jī)所構(gòu)造的CFITL，其語義解釋是基于分支時(shí)間觀念的非線性結(jié)構(gòu)有序CFG，并且有序CFG結(jié)構(gòu)作為系統(tǒng)實(shí)現(xiàn)模型，決定了系統(tǒng)的行為模型——Kripke結(jié)構(gòu)的拓?fù)洌虼薈FITL公式集成了系統(tǒng)實(shí)現(xiàn)的靜態(tài)結(jié)構(gòu)語義和動(dòng)態(tài)行為語義.計(jì)算機(jī)系統(tǒng)開發(fā)人員更習(xí)慣從系統(tǒng)實(shí)現(xiàn)的視面理解系統(tǒng)和規(guī)約系統(tǒng)，傳統(tǒng)上經(jīng)常采用謂詞邏輯對(duì)系統(tǒng)實(shí)現(xiàn)進(jìn)行規(guī)約，進(jìn)而基于規(guī)則系統(tǒng)進(jìn)行形式化的推理，而通過CFITL則可以采用自動(dòng)的算法方法對(duì)實(shí)現(xiàn)的各類屬性進(jìn)行驗(yàn)證，例如循環(huán)不變式；另外，通過區(qū)間，CFITL可以對(duì)系統(tǒng)實(shí)現(xiàn)結(jié)構(gòu)在各種粒度上進(jìn)行規(guī)約和推理.

5　總　　結(jié)

系統(tǒng)的動(dòng)態(tài)行為屬性由系統(tǒng)實(shí)現(xiàn)的靜態(tài)結(jié)構(gòu)屬性決定，研究關(guān)聯(lián)系統(tǒng)實(shí)現(xiàn)靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為屬性的規(guī)約形式和分析驗(yàn)證方法具有重要的應(yīng)用價(jià)值.本文基于CTL構(gòu)建了一種區(qū)間時(shí)序邏輯系統(tǒng)CFITL，該邏輯系統(tǒng)具有描述復(fù)雜的程序靜態(tài)結(jié)構(gòu)和動(dòng)態(tài)行為屬性的表達(dá)能力，通過一類受限的CFG及CFG誘導(dǎo)的位階函數(shù)給出了CFITL語義.位階函數(shù)用于解釋CFG的狀態(tài)的拓?fù)湫畔ⅲ闯绦虻撵o態(tài)結(jié)構(gòu)信息，定理1和定理2顯示它的構(gòu)造不單純由程序的抽象視圖CFG決定，還取決于CFG結(jié)構(gòu)相關(guān)的程序結(jié)構(gòu)因素.進(jìn)一步，本文詳細(xì)討論了CFITL的模型檢測問題，提出了具體的模型檢測算法，包括基于可達(dá)值狀態(tài)空間計(jì)算的模型檢驗(yàn)算法和基于SMT及CFITL公式重寫的有界模型檢驗(yàn)算法，并基于后一種算法初步實(shí)現(xiàn)了CFITL模型檢驗(yàn)器原型工具.后續(xù)工作將圍繞以下3方面展開：1)對(duì)CFITL邏輯系統(tǒng)的邏輯性質(zhì)進(jìn)行更深入地研究，包括表達(dá)能力和證明系統(tǒng)等；2)研究可行的抽象技術(shù)，適用于路徑敏感的CFITL模型檢驗(yàn)方法；3)基于C語言編程環(huán)境，完善VerTPCFG系統(tǒng)，集成各種復(fù)雜數(shù)據(jù)類型的處理功能及更豐富的可視化環(huán)境的支撐，使之能處理各類復(fù)雜程序.

[1]Ben-Ari M, Pnueli A, Manna M. The temoral logic of branching time[J]. Acta Informatica, 1981, 20(3): 207-226[2]Huth M, Ryan M. Logic in Computer Science: Modelling and Reasoning about System[M]. Cambridge, UK: Cambridge University Press, 2004[3]Kwiatkowska M. Model checking for probability and time: From theory to practice[C]Proc of the 18th IEEE Symp on Logic in Computer Science. Piscataway, NJ: IEEE, 2003: 351-360[4]Panangaden P. Labelled Markov Processes[M]. London: Imperial College Press, 2009[5]Clarke E M, Grumberg O, Peled D A. Model Checking[M]. Cambridge, MA: MIT Press, 1999[6]Burch J R, Clarke E M, McMillan K L, et al. Symbolic model checking: 1020states and beyond[J]. Information and Computation, 1992, 98(2): 142-170[7]Alur R, Courcourbetis C, Dill D. Model checking for real-time systems[C]Proc of the 5th Symp on Logic in Computer Science. Piscataway, NJ: IEEE, 1990: 414-425[8]Ball T, Majumdar R, Millstein T D, et al. Automatic predicate abstraction of C programs[C]Proc of the 22nd ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2001: 203-213[9]Clarke E M, Biere A, Raimi R. Bounded model checking using satisfiability solving[J]. Formal Methods in System Design, 2001, 19(1): 7-34[10]Miller S P, Whalen M W, Cofer D D. Software model checking takes off[J]. Communications of the ACM, 2010, 53(2): 58-64[11]Cordeiro L, Fischer B, Marques-Silva J. SMT-based bounded model checking for embedded ANSI-C software[J]. IEEE Trans on Software Engineering, 2012, 38(4): 957-974[12]Dill D L, Clarke E M. Automatic verification of asynchronous circuits using temporal logic[J]. IEE Proceedings E Computers and Digital Techniques, 1986, 133(5): 276-282[13]Bujang S D A, Selamat A. Verification of mobile SMS application with model checking agent[C]Proc of the 8th Int Conf on Intelligent Systems Design and Applications. Piscataway, NJ: IEEE, 2008: 217-222[14]Alur R, Jagadeesan L J, Kott J J, et al. Model-checking of real-time systems: A telecommunications application: Experience report[C]Proc of the 19th Int Conf on Software Engineering. Piscataway, NJ: IEEE, 1997: 514-524[15]Witkowski T, Blanc N, Kroening D, et al. Model checking concurrent Linux device drivers[C]Proc of the 22nd IEEEACM Int Conf on Automated Software Engineering. New York: ACM, 2007: 501-504[16]Chen H, Dean D, Wagner D. Model checking one million lines of C code[C]Proc of the 11th Symp on Network and Distributed System Security. Washington DC: Internet Society, 2004: 171-185[17]Necula G C. Proof-carrying code[C]Proc of the 24th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages. New York: ACM, 1997: 106-119[18]Bozga M, Iosif R, Perarnau S. Quantitative separation logic and programs with lists[J]. Journal of Automated Reasoning, 2010, 45(2): 131-156[19]L?ding C, Lutz C, Serre O. Propositional dynamic logic with recursive programs[J]. Journal of Logic and Algebraic Programming, 2007, 73(1): 51-69[20]Flanagan C, Leino C K R, Lillibridge M, et al. Extended static checking for Java[C]Proc of the 23rd ACM SIGPLAN Conf on Programming Language Design and Implementation. New York: ACM, 2002: 234-245[21]King J C. Symbolic execution and program testing[J]. Communications of the ACM, 1976, 19(7): 385-394[22]Ma K K, Phang K Y, Jeffrey S F. Directed symbolic execution[G]LNCS 6887: Proc of the 18th Int Conf on Statis Analysis. Berlin: Springer, 2011: 95-111[23]Saswat A, Godefroid P, Tillmann N. Demand-driven compositional symbolic execution[G]LNCS 4963: Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008: 367-381[24]Rosu G, Havelund K. Rewriting-based techniques for running verification[J]. Journal of Automated Software Engineering, 2005, 12(2): 151-197[25]Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories: From an abstract DPLL procedure to DPLL(T)[J]. Journal of ACM, 2006, 53(6): 937-977[26]B?hm C, Jacopini G. Flow diagrams, turing machines and languages with only two formation rules[J]. Communications of the ACM, 1966, 9(5): 366-371[27]Harel D. On folk theorems[J]. Communications of the ACM, 1980, 23(7): 379-389[28]Cousot P, Cousot R. Abstract interpretation: A unified lattice model for the static analysis of programs by construction or approximation of fixpoints[C]Proc of the 4th ACM SIGPLAN-SIGACT Symp on Principles of Programming Languages. New York: ACM, 1977: 238-252[29]Dams D, Gerth R, Grumberg O. Abstract interpretation of reactive systems[J]. ACM Trans of Program Language System, 1997, 19(2): 253-291[30]Zhang L, Malik S. The quest for efficient boolean satisfiability solvers[G]LNCS 2404: Proc of the 14th Int Conf on Computer Aided Verification. Berlin: Springer, 2002: 17-36[31]Zhang H. SATO: An efficient propositional prover[G]LNAI 1249: Proc of the 14th Int Conf on Automated Deduction. Berlin: Springer, 1997: 272-275[32]Moura L D. Z3: An efficient SMT solver[G]LNCS 4963: Proc of the 14th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2008: 337-340[33]Fraser G, Wotawa F. Using LTL rewriting to improve the performance of model checker based test case generation[C]Proc of the 3rd Workshop on Advances in Model Based Testing. New York: ACM, 2007: 64-74[34]Clarke D, Jeron T, Rusu V. STG: A symbolic test generation tool[G]LNCS 2280: Proc of the 8th Int Conf on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer, 2002: 152-173[35]Tang Zhisong, Zhao Chen. A temporal logic language oriented toward software engineering[J]. Journal of Software, 1994, 5(12): 1-16 (in Chinese)(唐稚松, 趙琛. 一種面向軟件工程的時(shí)序邏輯語言[J]. 軟件學(xué)報(bào), 1994, 5(12): 1-16)[36]Zhu Xueyang. The dual software architecture description framework XYZADL[J]. Journal Computer Research and Development, 2007, 44(9): 1485-1494 (in Chinese)(朱雪陽. 雙重軟件體系結(jié)構(gòu)描述框架XYZADL[J]. 計(jì)算機(jī)研究與發(fā)展， 2007, 44(9): 1485-1494)[37]Reynolds J C. Separation logic: A logic for shared mutable data structure[C]Proc of the 17th Annual IEEE Symp on Logic in Computer Science. Piscataway, NJ: IEEE, 2002: 55-74[38]Zhao J H, Li X D. Scope logic: An extension to hoare logic for pointers and recursive data structures[G]LNCS 8049: Theoretical Aspects of Computing. Berlin: Springer, 2013: 409-426[39]Balbiani P, Vakarelov D. PDL with intersection of programs: A complete axiomatization[J]. Journal of Applied Non-Classical Logics, 2003, 13(4): 231-276 [40]Chen Yiyun, Hua Baojian, Ge Lin, et al. A pointer logic for safety verification of pointer programs[J]. Chinese Journal of Computers, 2008, 31(3): 372-380 (in Chinese)(陳意云, 華保健, 葛琳, 等. 一種用于指針程序安全性證明的指針邏輯[J]. 計(jì)算機(jī)學(xué)報(bào), 2008, 31(3): 372-380)[41]Li Z P, Zhang Y, Chen Y Y. A shape graph logic and a shape system[J]. Journal of Computer Science & Technology, 2003, 28(6): 1063-1084[42]Li Guangyuan, Tang Zhisong. Representing and verifying reactvie systems with continuous-time temporal logic[J]. Chinese Journal of Computers, 2003, 26(11): 1424-1434 (in Chinese)(李廣元, 唐稚松. 反應(yīng)系統(tǒng)的連續(xù)時(shí)序邏輯表示和驗(yàn)證[J]. 計(jì)算機(jī)學(xué)報(bào), 2003, 26(11): 1424-1434)[43]Lin Chang, Qu Yang, Li Yajuan. Modeling, consistency and inference of extended interval temporal logic[J]. Chinese Journal of Computers, 2002, 25(12): 1338-1347 (in Chinese)(林闖, 曲楊, 李雅娟. 擴(kuò)展時(shí)段時(shí)序邏輯的模型、一致性和推理[J]. 計(jì)算機(jī)學(xué)報(bào), 2002, 25(12): 1338-1347)[44]Bresolin D, Monica D D, Montanari A, et al. The light side of interval temporal logic: The Bernays-Schonfinkel fragment of CDT[J]. Annals of Mathematics and Artificial Intelligence, 2014, 71(1): 11-39[45]Moszkowski B. Reasoning about digital circuits, STAN-CS-83-970[R]. Palo Alto, CA: Stanford University, 1983[46]Halpern J, Shoham Y. A propositional modal logic of time intervals[J]. Journal of ACM, 1991, 38(4): 935-962[47]Duan Zhenhua. An extended interval temporal logic and a framing technique for temporal logic programming[D]. Newcastle Upon Tyne, UK: Newcastle University, 1996[48]Tian Cong, Duan Zhenhua. Model checking rate monotone scheduling algorithm based on propositional projection temporal logic[J]. Journal of Software, 2011, 22(2): 211-221 (in Chinese)(田聰, 段振華. 基于命題投影時(shí)序邏輯的單調(diào)速率調(diào)度算法模型檢測[J]. 軟件學(xué)報(bào), 2011, 22(2): 211-221)

Chen Donghuo, born in 1974. PhD, lecturer. Member of China Computer Federation. His main research interests include program verification, model checking, and automated reasoning.

Liu Quan, born in 1969. Post doctor, professor and PhD supervisor. Senior member of China Computer Federation. His main research interests include intelli-gence information processing, automated reasoning, and machine learning.

Jin Haidong, born in 1973. PhD candidate, lecturer. His main research interests include reinforcement learning, and human-computer interaction.

Zhu Fei, born in 1978. PhD, associate professor. Member of China Computer Federation. His main research interests include reinforcement learning, text mining, and pattern recognition.

Wang Hui, born in 1968. PhD candidate, lecturer. Member of China Computer Federation. His main research interests include machine learning, and human-computer interaction.

A Temporal Logic with a Semantics Defined on the Static Structure and Dynamic Behavior of Program

Chen Donghuo1, Liu Quan1,2, Jin Haidong1, Zhu Fei1,2, and Wang Hui1

1(SchoolofComputerScienceandTechnology,SoochowUniversity,Suzhou,Jiangsu215006)2(KeyLaboratoryofSymbolicComputationandKnowledgeEngineering(JilinUniversity),MinistryofEducation,Changchun130012)

The paper presents an interval temporal logic—CFITL(control flow interval temporal logic) which is used to specify the temporal properties of abstract model of program, for example control flow graph, generally abbreviated to CFG. The targeted logic differs from the general sense of temporal logics, typically CTL and LTL, whose semantical models are defined in term of the state-based structures. The semantics of CFITL is defined on an ordered CFG structure, which encodes the static structure and dynamic behavior of program. The ordered CFGs are a subset of CFGs, and their topology can be summarized by partially ordered sets, such that the induced natural number intervals can be mapped onto the well-formed structures of program. In other words, the CFITL formulae have the ability of specifying the properties related to not only the dynamic behavior but also static structure of programs. After the syntax and semantics of CFITL are expounded, the problem of model checking over CFITL is detailedly discussed. Furthermore, two types of algorithms are designed: one is based on the computation of reachable state space as well as the another is based on bounded model checking employing the SMT(satisfiability modulo theories) solvers power. Because programs implemented by advanced programming languages inevitably involve complex abstract data types with unbounded domains and operators, and the semantics of CFITL is more complex than the one of CTL, the method of SMT based model checking is more practical than the method of direct search of state space. In the sequel, a prototype tool is implemented, and some case studies are conducted.

interval temporal logic; control flow graph (CFG); static structure of program; model checking; satisfiability modulo theories (SMT)

2015-05-14；

2016-02-16

國家自然科學(xué)基金項(xiàng)目(61272005,61303108,61373094,61472262,61502323,61502329)；江蘇省自然科學(xué)基金項(xiàng)目(BK2012616)；福建省自然科學(xué)基金項(xiàng)目(2014J01221)；江蘇省高校自然科學(xué)研究項(xiàng)目(13KJB520020)；吉林大學(xué)符號(hào)計(jì)算與知識(shí)工程教育部重點(diǎn)實(shí)驗(yàn)室項(xiàng)目(93K172014K04)；蘇州市應(yīng)用基礎(chǔ)研究計(jì)劃項(xiàng)目(SYG201422)

This work was supported by the National Natural Science Foundation of China (61272005, 61303108, 61373094, 61472262, 61502323, 61502329), the Natural Science Foundation of Jiangsu (BK2012616), the Natural Science Foundation of Fujian Province (2014J01221), the High School Natural Foundation of Jiangsu (13KJB520020), the Project Funded by the Key Laboratory of Symbolic Computation and Knowledge Engineering of Ministry of Education, Jilin University (93K172014K04), and the Suzhou Industrial Application of Basic Research Program (SYG201422).

劉全(quanliu@suda.edu.cn)

TP311