郭 婧， 徐中偉， 李麗梅

（1.同濟(jì)大學(xué) 電子與信息工程學(xué)院，上海 201804；2.九江學(xué)院 圖書(shū)館，江西 九江 332005）

隨著計(jì)算機(jī)技術(shù)的快速發(fā)展，人們對(duì)計(jì)算機(jī)軟件安全的要求不斷提高。模型檢測(cè)作為軟件安全檢測(cè)的重要工具被廣泛應(yīng)用。模型檢測(cè)［1］是軟件自動(dòng)驗(yàn)證技術(shù)，它是將要驗(yàn)證的系統(tǒng)用變遷系統(tǒng)來(lái)表示，通過(guò)驗(yàn)證來(lái)觀察該系統(tǒng)是否滿(mǎn)足需求。符號(hào)模型檢測(cè)［2］的出現(xiàn)使模型檢測(cè)得到更大的發(fā)展，可以將狀態(tài)集合用布爾函數(shù)來(lái)表示［3］。用有序二叉決策圖（ordered binary decision diagram，OBDD）來(lái)處理布爾函數(shù)，再通過(guò)優(yōu)化方法又可以處理更多的狀態(tài)數(shù)，使符號(hào)模型檢測(cè)能更好地投入實(shí)際應(yīng)用中［4］。OBDD仍無(wú)法避免狀態(tài)爆炸的問(wèn)題，無(wú)論變量順序如何，需要的存儲(chǔ)空間都是指數(shù)增長(zhǎng)的［5］。因此，可滿(mǎn)足性問(wèn)題（satisifiability problem，SAT）工具［6］得到廣泛應(yīng)用。限界模型檢測(cè)能解決OBDD的一些檢測(cè)問(wèn)題，并能給出檢測(cè)的反例［7－9］。

本文主要討論在軟件系統(tǒng)中進(jìn)行模型檢測(cè)，軟件程序被表示為嵌套樹(shù)和嵌套狀態(tài)機(jī)2種形式。嵌套樹(shù)表現(xiàn)了程序的所有執(zhí)行路線，嵌套狀態(tài)機(jī)則表現(xiàn)了程序語(yǔ)句之間的執(zhí)行關(guān)系［10－12］。在嵌套樹(shù)中定義μ演算（NT－μ），其基本語(yǔ)法單位為概要。嵌套樹(shù)中多個(gè)結(jié)點(diǎn)可以對(duì)應(yīng)于嵌套機(jī)中1個(gè)結(jié)點(diǎn)，概要之間存在等價(jià)關(guān)系而可以轉(zhuǎn)化成一個(gè)概要類(lèi)，從而在嵌套狀態(tài)機(jī)上提出以概要類(lèi)為基本單位的模型檢測(cè)。該方法能節(jié)省檢測(cè)時(shí)間，提高檢測(cè)效率。

1 基本概念

1.1 嵌套樹(shù)、嵌套狀態(tài)機(jī)的定義

定義1（嵌套樹(shù)） T＝（S，r，→，｜→）。其中，S為結(jié)點(diǎn)集合；r為根節(jié)點(diǎn)；→?S×S為邊的變遷關(guān)系集合；｜→?S× （S ∪｛∞｝）為跳躍邊的集合［13－14］。對(duì)于結(jié)點(diǎn)s，s→t表示s和t之間存在直接變遷關(guān)系，s為源結(jié)點(diǎn)，t為目標(biāo)結(jié)點(diǎn)；s｜→t表示s為調(diào)用結(jié)點(diǎn)，t為返回結(jié)點(diǎn)；s｜→∞表示s為調(diào)用結(jié)點(diǎn)且調(diào)用沒(méi)有返回。T中有限或無(wú)限道路表示為π＝s1s2…sn…，對(duì)所有i≥1，si→si＋1。

定義2（嵌套標(biāo)記樹(shù)） T＝（S，r，→，｜→，λ）。其中，λ：S→Σ；S為結(jié)點(diǎn)集合；Σ為嵌套樹(shù)標(biāo)記集合；λ為兩者之間的一個(gè)映射，其他符號(hào)同定義1。

為了方便理解，可以用η表示邊與結(jié)點(diǎn)之間的映射關(guān)系，η：E→｛call，return，local｝，E 為邊的集合，E 被分為調(diào)用邊（call）、返回邊（return）和局部邊（local），s→αt則η（s，t）＝α。調(diào)用邊表示邊的源結(jié)點(diǎn)為調(diào)用結(jié)點(diǎn)，返回邊表示邊的目標(biāo)結(jié)點(diǎn)是返回結(jié)點(diǎn)，其余的邊則為局部邊。

定義3（嵌套狀態(tài)機(jī)） M＝〈Vloc，Vcall，Vret，vin，κ，Δloc，Δcall，Δret〉。其中，Vloc為局部狀態(tài)有限集合；Vcall為調(diào)用狀態(tài)的有限集合；Vret為返回狀態(tài)的有限集合；vin為起始狀態(tài)?？偁顟B(tài)集合V＝Vloc∪Vcall∪Vret∪vin。κ：V→Σ表示狀態(tài)結(jié)點(diǎn)的標(biāo)記關(guān)系。局部變遷關(guān)系 Δloc? （Vloc∪Vret）×（Vloc∪Vcall）；調(diào) 用 變 遷 關(guān) 系 Δcall?Vcall×（Vloc∪Vcall）；返回變遷關(guān)系Δret? （Vloc∪Vret）×Vcall×Vret。

嵌套狀態(tài)機(jī)以嵌套樹(shù)為語(yǔ)法基礎(chǔ)，變遷關(guān)系被分為3類(lèi)。對(duì)于狀態(tài)結(jié)點(diǎn)s、v、t，如果（s，t）∈Δloc，則sl→oct；如果（s，t）∈Δcall，則sc→allt；如 果（s，t，v）∈Δret，則（s，t）→retv，t為最后一個(gè)未匹配的調(diào)用狀態(tài)結(jié)點(diǎn)，返回變遷關(guān)系表現(xiàn)了程序的控制權(quán)由源狀態(tài)結(jié)點(diǎn)交到返回狀態(tài)結(jié)點(diǎn)的過(guò)程。

嵌套狀態(tài)機(jī)的展開(kāi)可以表示為一個(gè)非順序的標(biāo)簽樹(shù)TV（M），該樹(shù)被看作執(zhí)行樹(shù)，為一個(gè)嵌套樹(shù)，即嵌套狀態(tài)機(jī)的展開(kāi)可以表示成唯一的嵌套樹(shù)。它的構(gòu)成形式如下：

（1）對(duì)于樹(shù)的根節(jié)點(diǎn)r，在M 中λ（r）＝vin。（2）如果s→αt，α∈｛call，loc｝，那么在 M 中λ（s）→αλ（t）。

（3）如果s→rett，并且存在狀態(tài)結(jié)點(diǎn)t′使t′｜→t，那么在 M 中（λ（s），λ（t′））→retλ（t）。

1.2 概要的定義

定義4（概要） 對(duì)于一個(gè)非負(fù)整數(shù)k，k種顏色的概要是一個(gè)數(shù)組〈s，U1，U2，…，Uk〉。其中，s為根結(jié)點(diǎn)；U1，U2，…，Uk為 ME（s）的子集，集合中顏色標(biāo)簽與集合中含有的結(jié)點(diǎn)數(shù)量相同。

一般固定點(diǎn)的計(jì)算是基于狀態(tài)本身的計(jì)算，而對(duì)于軟件來(lái)說(shuō)更注重功能的執(zhí)行。在本文中定義了一個(gè)新的語(yǔ)法結(jié)構(gòu)——概要，是針對(duì)過(guò)程內(nèi)容的計(jì)算。首先定義ME（s），即結(jié)點(diǎn)s的匹配出口結(jié)點(diǎn)集合。如果t為s的匹配出口結(jié)點(diǎn)必須滿(mǎn)足以下2個(gè)條件：

（1）如果s→＋t，且存在結(jié)點(diǎn)s′→＋s和s′｜→t。該條件表示s′為s 前驅(qū)結(jié)點(diǎn)，s′、s、t間有道路相連。

（2）不存在 結(jié) 點(diǎn)v、w，使s′→＋v→＋s→＋w 和v｜→w。該條件表示s′、s之間不存在結(jié)點(diǎn)v，該節(jié)點(diǎn)是調(diào)用結(jié)點(diǎn)，且相應(yīng)的返回結(jié)點(diǎn)、其他結(jié)點(diǎn)均可到達(dá)。

從定義來(lái)看，從結(jié)點(diǎn)s出發(fā)往樹(shù)的道路反方向“遇到”的第1個(gè)調(diào)用結(jié)點(diǎn)相對(duì)應(yīng)的返回結(jié)點(diǎn)集合，并從該集合中剔出與結(jié)點(diǎn)s無(wú)道路相連的結(jié)點(diǎn)，可得s的匹配出口結(jié)點(diǎn)集合。

1.3 嵌套樹(shù)的舉例

一段實(shí)例程序如下：

該段程序?qū)?yīng)的部分嵌套樹(shù)如圖1所示，因?yàn)樵摮绦蛑胁捎昧诉f歸調(diào)用以及循環(huán)，所以不可能把完整的嵌套樹(shù)畫(huà)出來(lái)。圖1中，結(jié)點(diǎn)｛wr｝表示write語(yǔ)句；結(jié)點(diǎn)｛en｝表示調(diào)用1段新的內(nèi)容；結(jié)點(diǎn)｛ex｝表示從現(xiàn)有內(nèi)容返回到原來(lái)的內(nèi)容；結(jié)點(diǎn)｛clr｝表示clear語(yǔ)句；結(jié)點(diǎn)｛prt｝表示print語(yǔ)句；結(jié)點(diǎn)｛end｝表示return語(yǔ)句；而結(jié)點(diǎn)｛ass｝表示變量被重新賦值。

圖1 實(shí)例程序的部分嵌套樹(shù)

L2、L3都是變量a被重新賦值，將其歸為一類(lèi)。該結(jié)點(diǎn)｛end｝僅僅是執(zhí)行return語(yǔ)句本身，并可以作為當(dāng)前內(nèi)容的結(jié)束，而結(jié)點(diǎn)｛ex｝則是返回原有的調(diào)用點(diǎn)后繼續(xù)執(zhí)行后面的內(nèi)容，因此在圖1中結(jié)點(diǎn)｛en｝與結(jié)點(diǎn)｛ex｝之間存在調(diào)用與返回的關(guān)系，兩者用跳躍邊（虛線箭頭）相連。對(duì)于該程序每條語(yǔ)句執(zhí)行了一個(gè)功能，如果一句語(yǔ)句執(zhí)行了多個(gè)功能，必須把語(yǔ)句斷開(kāi)進(jìn)行分解處理。對(duì)于調(diào)用語(yǔ)句來(lái)說(shuō)，有可能能返回，有可能無(wú)返回，即此程序有可能陷于被調(diào)用的無(wú)限循環(huán)中，用∞來(lái)表示。從樹(shù)的根結(jié)點(diǎn)到樹(shù)的葉子結(jié)點(diǎn)為程序的一條可執(zhí)行路線。

2 嵌套樹(shù)的μ－演算（NT－μ）

2.1 NT－μ的語(yǔ)法規(guī)則

根據(jù)樹(shù)結(jié)構(gòu)的邏輯公式［15］，構(gòu)建基于嵌套樹(shù)的μ演算公式。AP為原子命題的集合，var為變量的有限集合，｛M1，M2，…｝為可數(shù)有序的標(biāo)記集合。對(duì)于p∈AP，x，X∈var，k≥0，NT－μ的公式有多種基本形式，用“｜”符號(hào)隔開(kāi)，定義如下：

tt為所有結(jié)點(diǎn)都滿(mǎn)足的公式，即所有原子公式的全集，ff為tt的補(bǔ)集，即空公式集。設(shè)α為call、loc、ret則為當(dāng)前結(jié)點(diǎn)向前推α變遷關(guān)系。標(biāo)記被〈call〉和［call］形式的公式所限定，標(biāo)記記錄當(dāng)前內(nèi)容調(diào)用的點(diǎn)，當(dāng)新的被調(diào)用內(nèi)容執(zhí)行完畢返回時(shí)，返回標(biāo)記的點(diǎn)繼續(xù)執(zhí)行。

公式Φ最大標(biāo)記用mk（Φ）來(lái)表示，對(duì)于不同形式的公式有以下關(guān)系：

變量x被不動(dòng)點(diǎn)符號(hào)限定為μx.和νx.的形式，該變量稱(chēng)為非自由變量。公式的自由變量集合free（Φ）有以下關(guān)系：

公式滿(mǎn)足 mk（Φ）＝0、free（Φ）＝0分別為標(biāo)記封閉和自由變量封閉。如果兩者都成立，Φ整體被稱(chēng)為封閉的。

2.2 環(huán)境下NT－μ公式的語(yǔ)法意義

定義5（環(huán)境變量） 環(huán)境變量ε：free（Φ）→2S，Φ在環(huán)境中表示把Φ中的自由變量集合映射到嵌套樹(shù)中的概要集合。［［Φ］］εT表示在環(huán)境ε滿(mǎn)足Φ的T中的概要集合。一般T從當(dāng)前內(nèi)容能得到，所以可簡(jiǎn)寫(xiě)成［［Φ］］ε。

定義6（在環(huán)境下NT－μ公式的語(yǔ)法意義）對(duì)于一個(gè)概要s＝〈s，U1，U2，…，Uk〉，s∈［［Φ］］ε，當(dāng)且僅當(dāng)不同形式的公式滿(mǎn)足以下條件：

（1）Φ＝p∈AP，則p∈λ（s）。

（2）Φ＝?p，p∈AP，則p?λ（s）。

（3）Φ＝Φ1∨Φ2，則s∈ ［［Φ1］］ε或s∈［［Φ2］］ε。

（4）Φ＝Φ1∧Φ2，則s∈ ［［Φ1］］ε和s∈［［Φ2］］ε。

（5）Φ＝〈call〉Φ′｛φ1，φ2，…，φk｝或Φ＝［call］Φ′｛φ1，φ2，…，φk｝則分別表示s的一個(gè)調(diào)用后續(xù)結(jié)點(diǎn)t（sc→allt）、s的所有調(diào)用后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足對(duì)于以t為根結(jié)點(diǎn)的概要t〈t，V1，V2，…，Vn〉所有1≤i≤n，Vi＝ME（t）∩｛s′：〈s′，U1∩ME（s′），…，Uk∩ME（s′）〉∈［［φi］］ε｝。

（6）Φ＝〈loc〉Φ′或Φ＝［loc］Φ′則分別表示s的一個(gè)局部后續(xù)結(jié)點(diǎn)t（sl→oct）、s的所有局部后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足對(duì)于以t為根結(jié)點(diǎn)的概要t〈t，V1，V2，…，Vn〉，Vi＝ME（t）∩Ui且t∈［［Φ′］］ε。

（7）Φ＝〈ret〉Mi或Φ＝［ret］Mi則分別表示s的一個(gè)返回后續(xù)結(jié)點(diǎn)t（s→rett）、s的所有返回后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足t∈Ui。

（8）Φ＝〈loc〉Φ′或Φ＝［loc］Φ′則分別表示s的一個(gè)局部前續(xù)結(jié)點(diǎn)t（tl→ocs）、s的所有局部前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足以t為根結(jié)點(diǎn)的概要t〈t，V1，V2，…，Vk〉，對(duì)所有1≤i≤k，滿(mǎn)足Vi?Ui。

（9）Φ＝〈call〉Φ′｛φ1，φ2，…，φk｝或Φ＝［call］Φ′｛φ1，φ2，…，φk｝則分別表示s的一個(gè)調(diào)用前續(xù)結(jié)點(diǎn)t（tc→alls）、s的所有調(diào)用前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足對(duì)于以t為根結(jié)點(diǎn)的概要t〈t，V1，V2，…，Vn〉∈［［Φ′］］ε所有1≤i≤n，｛s′：〈s′，V1∩ME（s′），…，Vn∩ME（s′）〉∈［［φi］］ε｝?Ui。

（10）Φ＝〈ret〉Φ（Mi）或Φ＝［ret］Φ（Mi）則分別表示s的一個(gè)返回前續(xù)結(jié)點(diǎn)t（t→rets）、s的所有返回前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)，其中概要s＝〈s，U1，U2，…，Uk〉＝〈s〉且s∈Ui，概要t〈t，V1，V2，…，Vk〉滿(mǎn)足［［Φ′］］ε。

（11）Φ＝μx.Φ′則對(duì)一個(gè)滿(mǎn)足最小不動(dòng)點(diǎn)的概要，且包含該概要的集合S 滿(mǎn)足［［Φ′］］ε［x：＝S］?S。

（12）Φ＝νx.Φ′則對(duì)于一些 概要集合S 滿(mǎn)足S?［［Φ′］］ε［x：＝S］，且最大不動(dòng)點(diǎn)在集合S 中。

3 基于嵌套樹(shù)的模型檢測(cè)方法

3.1 模型檢測(cè)方法的定義

嵌套樹(shù)和嵌套狀態(tài)機(jī)的區(qū)別在于：嵌套樹(shù)的結(jié)點(diǎn)集合有可能是無(wú)限的，是程序的所有可能執(zhí)行路線；而嵌套狀態(tài)機(jī)是語(yǔ)句執(zhí)行之間的關(guān)系，它的狀態(tài)結(jié)點(diǎn)集合是有限的。嵌套樹(shù)TV（M）（簡(jiǎn)寫(xiě)為T(mén)（M））是嵌套狀態(tài)機(jī)M的展開(kāi)形式。在嵌套狀態(tài)機(jī)的基礎(chǔ)上進(jìn)行模型檢測(cè)比在嵌套樹(shù)上進(jìn)行優(yōu)勢(shì)明顯。嵌套樹(shù)的基本單位是概要〈s，U1，U2，…，Uk〉，U1，U2，…，Uk為 ME（S）的子集。FC（s）表示離結(jié)點(diǎn)s最近的前驅(qū)調(diào)用結(jié)點(diǎn)（如果不存在FC（s）＝⊥），它的返回結(jié)點(diǎn)集合即為 ME（s）。嵌套樹(shù)結(jié)點(diǎn)的不同標(biāo)簽對(duì)應(yīng)于嵌套狀態(tài)機(jī)的不同狀態(tài)結(jié)點(diǎn)，因此可以基于嵌套狀態(tài)機(jī)來(lái)判斷概要的等價(jià)性，定義如下：

概要S＝〈s，U1，U2，…，Uk〉和概要S′＝〈s′，U′1，U2′，…，Uk′〉等 價(jià)，可 寫(xiě) 作 S≡MS′，簡(jiǎn)寫(xiě)為S≡S′，滿(mǎn)足以下條件：

（1）λ（s）＝λ（s′）。

（2）λ（FC（s））＝λ（FC（s′））。

（3）對(duì)于1≤i≤k，存在一個(gè)Ωi：Ui→U′i，任意結(jié)點(diǎn)u∈Ui都有λ（u）＝λ（Ωi（u）），且Ui中結(jié)點(diǎn)個(gè)數(shù)與Ui′中結(jié)點(diǎn)個(gè)數(shù)相等。

由此可以看出，2個(gè)概要等價(jià)除了要有相同的“規(guī)?！保叭亟Y(jié)點(diǎn)”（根節(jié)點(diǎn)、最近前驅(qū)調(diào)用結(jié)點(diǎn)、匹配出口結(jié)點(diǎn)子集）的標(biāo)簽也要相等。標(biāo)簽相等即概要中結(jié)點(diǎn)對(duì)應(yīng)于嵌套狀態(tài)機(jī)中同一個(gè)結(jié)點(diǎn)。判斷概要結(jié)點(diǎn)s對(duì)應(yīng)為將嵌套樹(shù)中結(jié)點(diǎn)v為λ（s）＝κ（v）。概要全集S分為一個(gè)個(gè)概要集合，每個(gè)概要集合中的概要均等價(jià)，即將概要全集劃分為互不相交的等價(jià)類(lèi)。如果概要集合是等價(jià)類(lèi)，那么記作該概要是等價(jià)封閉的。環(huán)境變量ε：free（Φ）→2S，如果自由變量集合free（Φ）中每個(gè)自由變量映射的概要集合都是等價(jià)封閉的，則該環(huán)境變量也是等價(jià)封閉的。

定理1 在等價(jià)封閉的環(huán)境ε中，對(duì)于NT－μ公式Φ，2個(gè)等價(jià)的概要S、S′中有一個(gè)屬于，則另一個(gè)也屬于（一般簡(jiǎn)寫(xiě)為［［Φ］］ε，嵌套樹(shù)T（M）默認(rèn)為當(dāng)前嵌套樹(shù)）。

定義7（概要類(lèi)的模型檢測(cè)） 設(shè)NT－μ公式Φ，一個(gè) 概 要 類(lèi) 為 U ＝ 〈v，v′，V1，V2，…，Vk〉，F(xiàn)CM（s，s′）＝true。對(duì)1≤i≤k，Vi?MEM（v，v′）。概要類(lèi)標(biāo)注為SC。嵌套狀態(tài)機(jī)中環(huán)境變量εSC為：free（Φ）→2SC，將公式中自由變量映射成概要類(lèi)集合，表示在環(huán)境εSC下嵌套狀態(tài)機(jī)M中滿(mǎn)足Φ 的概要類(lèi)集合（一般簡(jiǎn)寫(xiě)為［［Φ］］εSC，默認(rèn)為當(dāng)前狀態(tài)機(jī)）。

（3）Φ＝Φ1∨Φ2則∪。

（4）Φ＝Φ1∧Φ2則∩。

（5）Φ＝〈call〉Φ′｛φ1，φ2，…，φk｝或Φ＝［call］Φ′｛φ1，φ2，…，φk｝則分別表示v的一個(gè)調(diào)用后續(xù)結(jié)點(diǎn)、s的所有調(diào)用后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足對(duì)于以t為根結(jié)點(diǎn)的概要類(lèi)t＝〈t，v，V1′，V2′，…，Vn′〉∈ ［［Φ′］］εSC，對(duì) 所 有 1≤i≤n、u∈Vi′有〈u，v′，U1，U2，…，Uk〉∈［［φi］］εSC，且對(duì)于1≤j≤k，Uj＝Vj∩ME（u，v′）。

（6）Φ＝〈loc〉Φ′或Φ＝［loc］Φ′則分別表示s的一個(gè)局部后續(xù)結(jié)點(diǎn)t（vl→oct）、s的所有局部后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足對(duì)于以t為根結(jié)點(diǎn)的概要類(lèi)t＝〈t，v′，U1，U2，…，Uk〉，Ui＝ME（t，v′）∩Vi且t ∈［［Φ′］］εSC。

（7）Φ＝〈ret〉Mi或Φ＝［ret］Mi則分別表示v 的一個(gè)返回后續(xù)結(jié)點(diǎn)t（（v，v′）r→ett）、s的所有返回后續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足t∈Vi。

（8）Φ＝μx.Φ′，則對(duì)最小不動(dòng)點(diǎn)的計(jì)算為對(duì)于［［Φ］］ε［X：＝x］，首先將?帶入x，直到該式的值SC不再改變得到最小不動(dòng)點(diǎn)的概要類(lèi)集合。

（9）Φ＝νx.Φ′，則對(duì)最大不動(dòng)點(diǎn)的計(jì)算為對(duì)于［［Φ］］ε［X：＝x］，首先將概要類(lèi)全集 SC帶入x，SC直到該式的值不再改變得到最大不動(dòng)點(diǎn)的概要類(lèi)集合。

分析前驅(qū)關(guān)系NT－μ前驅(qū)公式，向前變遷產(chǎn)生的概要類(lèi)中U1，U2，…，Un的范圍會(huì)擴(kuò)大。因此，無(wú)法具體限制概要類(lèi)的范圍，只能在已知概要類(lèi)的情況下判斷是否符合公式，具體判斷如下：

情形1 Φ＝〈loc〉Φ′或Φ＝［loc］Φ′則分別表示v的一個(gè)局部前續(xù)結(jié)點(diǎn)t（tl→ocv）、v的所有局部前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t滿(mǎn)足以t為根結(jié)點(diǎn)的概要類(lèi)t＝〈t，v′，U1，U2，…，Uk〉，對(duì)所有1≤i≤k滿(mǎn)足Ui?Vi。

情形2 Φ＝〈call〉Φ′｛φ1，φ2，…，φk｝或Φ＝［call］Φ′｛φ1，φ2，…，φk｝則分別表示v的一個(gè)調(diào)用前續(xù)結(jié)點(diǎn)v′（v′c→allv）、v的所有調(diào)用前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)v′滿(mǎn)足對(duì)于以v′為根結(jié)點(diǎn)概要類(lèi)〈v′，s，U1，U2，…，Un〉∈［［Φ′］］εSC（FCM（v，s）＝true）所有1≤i≤n，｛s′：〈s′，v′，U1∩ME（s′，v′），…，Un∩ME（s′，v′）〉∈［［φi］］εSC｝?Vi。

情形3 Φ＝〈ret〉Φ′（Mi）或Φ＝［ret］Φ′（Mi）則分別表示v 的一個(gè)返回前續(xù)結(jié)點(diǎn)t（（t，v′）→retv）、v的所有返回前續(xù)結(jié)點(diǎn)集合中的結(jié)點(diǎn)t，概要類(lèi)〈t，v′，V1，V2，…，Vk〉滿(mǎn)足［［Φ′］］εSC且v∈Vi。

分析概要類(lèi)的環(huán)境變量εSC為：free（Φ）→2SC，映射到概要類(lèi)子集。而如果ε（X）是等價(jià)封閉的，表示每個(gè)自由變量映射的概要子集都是等價(jià)封閉的，那么映射到環(huán)境變量εSC中為等價(jià)類(lèi)。

3.2 應(yīng)用實(shí)例

在嵌套狀態(tài)機(jī)中，用狀態(tài)s1、s2、s3、s4、s5、s6、s7分別表示行L1、L2、L3、L4、L5、L6、L7。用s4′表示程序返回到原來(lái)調(diào)用執(zhí)行點(diǎn)。局部狀態(tài)集合為s1、s2、s3、s5、s6、s7，調(diào)用狀態(tài)為s4，返回狀態(tài)為s4′，起始狀態(tài)為s1。這些狀態(tài)以行為單位，對(duì)于循環(huán)、條件語(yǔ)句只作為控制語(yǔ)句來(lái)執(zhí)行，作為判斷語(yǔ)句執(zhí)行的條件，而語(yǔ)句不執(zhí)行任何具體的動(dòng)作，因此不作為狀態(tài)。狀態(tài)與嵌套樹(shù)的標(biāo)簽有以下對(duì)應(yīng)關(guān)系：κ（s1）＝wr，κ（s2）＝κ（s3）＝mod，κ（s4）＝en，κ（s5）＝clr，κ（s6）＝prt，κ（s7）＝end，κ（s4′）＝ex。嵌套狀態(tài)機(jī)Mp的變遷如下：

嵌套狀態(tài)機(jī)Mp如圖2所示，返回關(guān)系用虛線表示。

圖2 實(shí)例程序的嵌套狀態(tài)機(jī)

若要檢測(cè)需求 AFcprt＝μx.（prt∨（［loc］x∧［call］δ｛x｝）），其中δ＝μy.（prt∨ （［ret］R1∧［loc］y∧［call］y｛y｝））。先找尋滿(mǎn)足δ的概要類(lèi)，最小不動(dòng)點(diǎn)y的值帶入?。第1步得到T1＝｛〈s6，s4，｛s4′｝〉，〈s7，s4，｛s4′｝〉｝，第2步將T1帶入y不再變化。計(jì)算 AFcprt＝μx.（prt∨（［loc］x∧［call］δ｛x｝）），T1′＝｛〈s6，s4，｛s4′｝〉｝即為所求。

4 結(jié)束語(yǔ)

本文介紹了嵌套樹(shù)表示程序的方法，并給出了嵌套狀態(tài)機(jī)的定義。引出了嵌套樹(shù)的μ－演算（NT－μ）完整的語(yǔ)法結(jié)構(gòu)，該語(yǔ)法結(jié)構(gòu)有個(gè)基本單位——概要，概要是以調(diào)用返回關(guān)系為基礎(chǔ)來(lái)表示程序的執(zhí)行過(guò)程，并考慮了可能同時(shí)執(zhí)行的其他過(guò)程。并在此基礎(chǔ)上討論了嵌套狀態(tài)機(jī)上概要類(lèi)的模型檢測(cè)。嵌套狀態(tài)機(jī)的結(jié)點(diǎn)和概要類(lèi)都是有限的，因此該方法比基于嵌套樹(shù)的模型檢測(cè)的效率有所提高。

［1］ Clarke E，Grumberg O，Peled D.Model checking［M］.MIT Press，1999：1－20.

［2］ Biere A，Cimatti A，Clarke E，et al.Symbolic model checking without BDDs［C］／／Proc of TACAS’99，Netherlands.Springer－Verlag，1999：193－207.

［3］ Brayant R E.Graph－based algorithms for Boolean function manipulation［J］.IEEE Transaction on Computers，1986，35（8）：677－691.

［4］ Boiling B，Wegener I.Improving the variable ordering of OBDD is NP－complete［J］.IEEE Transaction Computers，1996，45（9）：993－1001.

［5］ Biere A，Cimatti A，Clarke E，et al.Advances in computers［M］.Academic Press，2003：42－60.

［6］ Alessandro A，Luca C.SAT－based model－checking for security protocols analysis［J］.International Journal of Information Security，2008，7（1）：3－32.

［7］ Latvala T，Biere A，Heljanko K，et al.Simple is better：Efficient bounded model checking for past LTL［C］／／International Conference on Verification，Model checking，and Abstract Interpretation，F(xiàn)rance.Springer－Verlag，2005：380－395.

［8］ Penczek W，Wozna B，Zbrzezny A.Bounded model checking for the universal fragment of CTL［J］.Fundamental Informaticae，2002，51（1）：135－156.

［9］ Wozna B.ACTL＊ properties and bounded model checking［J］.Fundamental Informaticae，2004，62（2）：1－23.

［10］ Reps T，Horaitz S，Sagiv S.Precise interprocedural dataflow analysis via graph reachabiliy［C］／／Proceedings of the ACM Symposium on Principles of Programming Languages.San Francisco：ACM，1995：49－61.

［11］ 韓江洪，劉征宇，劉曉平，等.工業(yè)控制安全研究綜述［J］.合肥工業(yè)大學(xué)學(xué)報(bào)：自然科學(xué)版，2010，33（2）：161－168，173.

［12］ Alur R，Chaudhuri S，Madhusudan P.Languages of nested trees［C］／／Proceedings of the Symposium on Computer－Aided erification.IEEE，2006：329－342.

［13］ Alur R，Chaudhuri S，Madhusudan P.Software model checking using languages of nested trees［J］.ACM Transactions on Programming Languages and Systems，2011，33（5）：1501－1545.

［14］ Walukiewicz I.Monadic second－order logic on tree－like structures［J］.Theor Comput Sci，2002，275（1／2）：311－346.

［15］ Jensen T，Metayer D L，Thorn T.Verification of control flow based security properties［C］／／Proceedings of the IEEE Symposium on Security and Privacy.IEEE，1999：89－103.