命題投影時序邏輯的完備公理系統(tǒng)與形式驗(yàn)證.pdf

1、作為一種形式化驗(yàn)證的主流方法，定理證明已被成功地應(yīng)用于軟件和硬件的驗(yàn)證。不同于模型檢測技術(shù)，定理證明與狀態(tài)無關(guān)，不存在狀態(tài)空間爆炸問題，因此可用來驗(yàn)證有窮狀態(tài)系統(tǒng)、無窮狀態(tài)系統(tǒng)以及參數(shù)化系統(tǒng)。它將系統(tǒng)和期望的性質(zhì)均描述為邏輯公式，然后利用一組公理和推理規(guī)則去構(gòu)造系統(tǒng)公式蘊(yùn)含性質(zhì)公式的證明，從而達(dá)到驗(yàn)證系統(tǒng)滿足性質(zhì)的目的。本文研究了基于命題投影時序邏輯的定理證明技術(shù)。命題投影時序邏輯(Propositional Projection Te

2、mporal Logic,PPTL)基于命題區(qū)間時序邏輯(Propositional Interval Temporal Logic,PITL)引入了新投影操作符prj，投影加操作符prj-⊕，以及無窮模型。PPTL同時具備可判定性和完全ω正則表達(dá)力，能夠描述順序、并行、選擇、循環(huán)等多種程序行為。為充分利用二者的優(yōu)點(diǎn)，提出了一個完備的命題投影時序邏輯公理系統(tǒng)，包括公理和推理規(guī)則，常用定理以及合理性和完備性證明。使得對待驗(yàn)證系統(tǒng)的建模，期

3、望性質(zhì)的描述，以及系統(tǒng)模型滿足期望性質(zhì)的驗(yàn)證可在同一符號體系下完成。其中合理性證明基于PPTL模型理論，完備性的證明依賴于不動點(diǎn)理論和任何PPTL公式均可被轉(zhuǎn)化成范式這一事實(shí)。給出的進(jìn)程互斥用例說明了這一方法的可行性。
　　基于給出的命題投影時序邏輯的公理系統(tǒng)，本文研究了實(shí)時系統(tǒng)的驗(yàn)證方法。以最早截止期優(yōu)先調(diào)度算法為例，驗(yàn)證算法對任務(wù)集可行性的充要條件，即Liu and Layland定理。用建模、仿真和驗(yàn)證語言(Modeling

4、,Simulation and Verification Language,MSVL)描述算法，用PPTL公式描述性質(zhì)，由于實(shí)現(xiàn)該算法的MSVL程序可被轉(zhuǎn)化為PPTL公式，則可采用PPTL公理系統(tǒng)對其驗(yàn)證。
　　除此，本文還研究了基于命題投影時序邏輯公理系統(tǒng)的硬件系統(tǒng)驗(yàn)證。以全加器和超前進(jìn)位加法器為例說明了基于PPTL公理系統(tǒng)對硬件驗(yàn)證的一般方法。
　　隨著多核處理器的發(fā)展，多核并行程序的開發(fā)、規(guī)范及驗(yàn)證已經(jīng)成為一個挑戰(zhàn)。為

5、描述多核并行程序不同進(jìn)程之間的自治、并發(fā)和通信，基于投影時序邏輯(Projection Temporal Logic,PTL)提出了柱面計算模型(Cylinder Computation Model,CCM)。柱面計算模型以細(xì)粒度區(qū)間為公共時間軸，圍繞在它周圍的粗粒度區(qū)間形成一個柱面。執(zhí)行在粗粒度區(qū)間上的進(jìn)程被看做分布在不同核上的進(jìn)程，這些進(jìn)程在公共的投影點(diǎn)上完成通信，因此該模型可用來描述任意多核的并行計算。研究了CCM的模型理論，包括