命題投影時序邏輯的完備公理系統與形式驗證.pdf

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

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

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

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

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