作為一種形式化驗證的主流方法，定理證明已被成功地應用于軟件和硬件的驗證。不同于模型檢測技術，定理證明與狀態(tài)無關，不存在狀態(tài)空間爆炸問題，因此可用來驗證有窮狀態(tài)系統(tǒng)、無窮狀態(tài)系統(tǒng)以及參數(shù)化系統(tǒng)。它將系統(tǒng)和期望的性質均描述為邏輯公式，然后利用一組公理和推理規(guī)則去構造系統(tǒng)公式蘊含性質公式的證明，從而達到驗證系統(tǒng)滿足性質的目的。本文研究了基于命題投影時序邏輯的定理證明技術。命題投影時序邏輯(Propositional Projection Temporal Logic, PPTL)基于命題區(qū)間時序邏輯(Propositional Interval Temporal Logic,PITL)引入了新投影操作符prj，投影加操作符prj⊕，以及無窮模型。PPTL同時具備可判定性和完全ω正則表達力，能夠描述順序、并行、選擇、循環(huán)等多種程序行為。為充分利用二者的優(yōu)點，提出了一個完備的命題投影時序邏輯公理系統(tǒng)，包括公理和推理規(guī)則，常用定理以及合理性和完備性證明。使得對待驗證系統(tǒng)的建模，期望性質的描述，以及系統(tǒng)模型滿足期望性質的驗證可在同一符號體系下完成。其中合理性證明基于PPTL模型理論，完備性的證明依賴...

【文章頁數(shù)】：131 頁

【學位級別】：博士

【文章目錄】：
作者簡介
摘要
Abstract
1 Introduction
    1.1 Formal Methods
        1.1.1 Formal Specification
        1.1.2 Formal Verification
            1.1.2.1 Model Checking
            1.1.2.2 Theorem Proving
    1.2 Temporal Logic and Temporal Logic Programming
        1.2.1 Temporal Logic
        1.2.2 Temporal Logic Programming
    1.3 Contributions
    1.4 The Organization of the Thesis
2 Propositional Projection Temporal Logic
    2.1 Syntax and Semantics
        2.1.1 Syntax
        2.1.2 Semantics
    2.2 Precedence Rules and Properties of Formulas
        2.2.1 Precedence Rules
        2.2.2 Properties of Formulas
    2.3 Discussion
        2.3.1 Similarities
        2.3.2 Specific Characteristics
    2.4 Derived Formulas and Logical Laws
        2.4.1 Derived Formulas
        2.4.2 Logical Laws
    2.5 Conclusion
3 The Proof System for Propositional Projection Temporal Logic
    3.1 Proof System
        3.1.1 Axioms
        3.1.2 Inference Rules
        3.1.3 Formal Proof and Theorems
    3.2 Soundness
    3.3 Completeness
    3.4 A Case Study — Mutual Exclusion
    3.5 Conclusion
4 Cylinder Computation Model
    4.1 Projection Temporal Logic
        4.1.1 Syntax
        4.1.2 Semantics
    4.2 Modeling, Simulation and Verification Language
        4.2.1 Framing
        4.2.2 Expressions and Statements
        4.2.3 Normal Form of MSVL
    4.3 Sequence Expression
    4.4 CCM
    4.5 Operational Semantics
        4.5.1 Operational Semantics of MSVL
        4.5.2 Operational Semantics of CCM
    4.6 Implementation of CCM in MSVL
        4.6.1 MSVL Interpreter
        4.6.2 Implementation of CCM
            4.6.2.1 Reduction of Parallel
            4.6.2.2 Reduction of Over
    4.7 A Case Study — Word Processor
    4.8 Conclusion
5 Formal Verification of Real Time Systems
    5.1 Deadline Driven Scheduler
    5.2 Formalization of the Deadline Driven Scheduler
    5.3 Proof of Liu and Layland’s Theorem
        5.3.1 Formal Proof of Theorems
        5.3.2 Lemmas
        5.3.3 Sufficiency
        5.3.4 Necessity
    5.4 Conclusion
6 Formal Verification of Hardware Designs
    6.1 Verification of the Full Adder
        6.1.1 Full Adder
        6.1.2 Modeling and Verification of the Full Adder
    6.2 Formal Verification of Carry Lookahead Adder
        6.2.1 Carry Lookahead Adder
        6.2.2 Modeling and Verification of the Carry Lookahead Adder
    6.3 Conclusion
7 Conclusions and Future Works
    7.1 Conclusions
    7.2 Future Works
Acknowledgements
References
Finished Papers



本文編號：3969632