命題投影時(shí)序邏輯符號模型檢測及其應(yīng)用研究.pdf

1、模型檢測是一種驗(yàn)證軟硬件系統(tǒng)、多智能體系統(tǒng)、通信協(xié)議和嵌入式系統(tǒng)等的重要形式化方法。它將待驗(yàn)證系統(tǒng)建模為有限狀態(tài)機(jī)，如Kripke結(jié)構(gòu)、狀態(tài)-遷移系統(tǒng)或自動機(jī)等，將系統(tǒng)期望的性質(zhì)描述為時(shí)序邏輯公式；然后，自動化窮舉搜索系統(tǒng)行為以確定待驗(yàn)證系統(tǒng)是否滿足期望的性質(zhì)。然而，現(xiàn)有模型檢測方法大多基于顯式狀態(tài)空間描述和操作，即便使用動態(tài)狀態(tài)空間構(gòu)建和偏序規(guī)約等優(yōu)化技術(shù)，可驗(yàn)證系統(tǒng)的規(guī)模仍然十分有限。在實(shí)際設(shè)計(jì)中系統(tǒng)模型的大小往往隨著并發(fā)組件的數(shù)目

2、呈現(xiàn)指數(shù)級增長，這一問題構(gòu)成了將模型檢測技術(shù)應(yīng)用于實(shí)際設(shè)計(jì)的主要瓶頸。此外，模型檢測的形式化規(guī)范語言（如計(jì)算樹邏輯和線性時(shí)序邏輯等）的表達(dá)能力不足，描述順序、并發(fā)和循環(huán)等性質(zhì)較為困難，或者根本無法描述這些性質(zhì)。因此，本文研究了命題投影時(shí)序邏輯的符號模型檢測技術(shù)及其應(yīng)用。
　　命題投影時(shí)序邏輯(Propositional Projection Temporal Logic，PPTL)是對命題區(qū)間時(shí)序邏輯(Propositional

3、Interval Temporal Logic，PITL)的擴(kuò)展。它引入了新的時(shí)序操作符且被證明具有完全正則表達(dá)能力，能夠方便的描述順序、并行、選擇、時(shí)間敏感和周期性等多種并發(fā)的系統(tǒng)性質(zhì)。符號模型檢測是一種應(yīng)對顯式狀態(tài)模型檢測中容易出現(xiàn)的狀態(tài)空間爆炸問題的有效方法。它將待驗(yàn)證系統(tǒng)模型和系統(tǒng)期望的性質(zhì)描述為布爾方程，然后通過基于規(guī)約有序二叉決策圖的搜索算法查找系統(tǒng)模型中滿足期望性質(zhì)的狀態(tài)集合?；赑PTL和符號模型檢測方法的優(yōu)點(diǎn)，提出了一

4、個(gè)使用符號模型檢測方法驗(yàn)證PPTL規(guī)范的統(tǒng)一框架。在該框架中，將待驗(yàn)證系統(tǒng)建模為Kripke結(jié)構(gòu)M=(S，I,R,L)，其中S表示有限狀態(tài)集合，I表示初始狀態(tài)集合，R∈S×S表示集合S上的狀態(tài)遷移關(guān)系，標(biāo)記函數(shù)L用每個(gè)狀態(tài)下成立的原子命題標(biāo)記該狀態(tài)；將系統(tǒng)期望的性質(zhì)描述為PPTL公式φ。然后，將期望性質(zhì)的否定形式-φ轉(zhuǎn)化為它對應(yīng)的范式。由于范式是構(gòu)建標(biāo)記范式圖(Labeled Normal Form Graph，LNFG)的基礎(chǔ)，且LN

5、FG包含了目標(biāo)公式所有可能的模型。因此，可以求得狀態(tài)集合Sat-φ，使得對于該集合中的任意狀態(tài)s，s包含于S且公式-φ在模型M中任何以s開頭的路徑上成立。通過這種方式可以將檢查系統(tǒng)模型M是否滿足期望性質(zhì)φ的問題等價(jià)為檢查初始狀態(tài)集合I中滿足?φ的子集SAT(-φ)∩I是否為空的問題。事實(shí)上，通過進(jìn)一步分析發(fā)現(xiàn)PPTL符號模型檢測方法的時(shí)間雜度為O{(log|V(φ)|}×|V(φ)|×(|R|+|S|))，其中|V(φ)|為公式φ的LN

6、FG中頂點(diǎn)的數(shù)目，而|R|+|S|表示模型M的大小。此外，通過驗(yàn)證實(shí)例說明了PPTL的符號模型檢測方法的可行性。
　　基于給出的PPTL符號模型檢測方法，本文研究了實(shí)時(shí)與嵌入式計(jì)算系統(tǒng)的形式化驗(yàn)證方法。以單調(diào)速率調(diào)度算法和延遲單調(diào)速率調(diào)度算法為例，驗(yàn)證了上述算法對任務(wù)集可調(diào)度性的充要條件。將任務(wù)集在單調(diào)速率調(diào)度算法和延遲單調(diào)速率調(diào)度算法調(diào)度下的行為建模為Kripke結(jié)構(gòu)，將調(diào)度算法的可調(diào)度性描述為PPTL公式，然后調(diào)用PPTL符號

7、模型檢測方法對任務(wù)集在單調(diào)速率和延遲單調(diào)速率調(diào)度算法下的可調(diào)度性分別進(jìn)行描述和驗(yàn)證。
　　近幾年來，基于線性時(shí)序邏輯和分支時(shí)序邏輯的符號模型檢測方法是當(dāng)前形式化驗(yàn)證領(lǐng)域最為活躍的研究課題之一，并實(shí)現(xiàn)了相應(yīng)的符號模型檢測工具，如SMV、NuSMV和NuSMV2等。但是，上述工具均受制于形式化規(guī)范語言的表達(dá)能力，無法完整描述順序、并行、選擇、時(shí)間敏感和周期性等性質(zhì)。此外，上述符號模型檢測工具均不支持以PPTL公式描述的規(guī)范。因此，本文