命题投影时序逻辑的完备公理系统与形式验证

发布时间：2024-05-11 06:03

　　作为一种形式化验证的主流方法，定理证明已被成功地应用于软件和硬件的验证。不同于模型检测技术，定理证明与状态无关，不存在状态空间爆炸问题，因此可用来验证有穷状态系统、无穷状态系统以及参数化系统。它将系统和期望的性质均描述为逻辑公式，然后利用一组公理和推理规则去构造系统公式蕴含性质公式的证明，从而达到验证系统满足性质的目的。本文研究了基于命题投影时序逻辑的定理证明技术。命题投影时序逻辑(Propositional Projection Temporal Logic, PPTL)基于命题区间时序逻辑(Propositional Interval Temporal Logic,PITL)引入了新投影操作符prj，投影加操作符prj⊕，以及无穷模型。PPTL同时具备可判定性和完全ω正则表达力，能够描述顺序、并行、选择、循环等多种程序行为。为充分利用二者的优点，提出了一个完备的命题投影时序逻辑公理系统，包括公理和推理规则，常用定理以及合理性和完备性证明。使得对待验证系统的建模，期望性质的描述，以及系统模型满足期望性质的验证可在同一符号体系下完成。其中合理性证明基于PPTL模型理论，完备性的证明依赖...

【文章页数】：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