打结不变的命题投影时序逻辑与模型检测

发布时间：2021-05-11 06:05

　　本文提出了打结不变的命题投影时序逻辑,介绍了基于该逻辑的模型检测方法,并采用该方法验证了无条件安全通信协议。命题投影时序逻辑（PPTL）可表达所有ω-正则式其表达能力强于其他线性命题时序逻辑（如PTLL）,此外作为性质描述语言,其中的projection和chop算子使得性质定义更为灵活,因此PPTL适用于有穷状态并发系统的描述和验证。基于PPTL的模型检测方法近年来被提出,然而其作为一种形式化验证方法同样要面临状态爆炸问题。为此,本文定义了PPTL的打结不变子逻辑（记作PPTLst）,证明了PPTLst可表达所有PPTL可表达的打结不变性质。由于PPTLst定义的性质对系统中打结等价的行为不做区别,所以在偏序规约验证中,针对打结等价类只需验证其中的一个行为而不必验证等价类中的所有行为。因此支持PPTLst的偏序归约技术可避免遍历整个系统状态空间。基于该思想本文实现了支持基于PPTLst偏序规约的模型检测器。此外,PPTLst还可作为性质描述语言用于组合验证。其包含的projection和chop算子允许将性质定义在系统路径中受关注的状态上,并且由这些状态构成的抽象路径与原路径打结等价... 

【文章来源】：西安电子科技大学陕西省 211工程院校 教育部直属院校

【文章页数】：131 页

【学位级别】：博士

【文章目录】：
摘要
Abstract
1 Introduction
    1.1 Temporal Logic and Model Checking
    1.2 Existing problems and Research Focuses
    1.3 Thesis Overview and Contributions
2 Background
    2.1 Propositional Projection Temporal Logic
    2.2 Model Checking Using Automata
        2.2.1 ω-Automata
        2.2.2 Specification using ω-Automata
    2.3 Model Checking Using PPTL Specification
    2.4 Summary
3 Upper Bound of Complexity for PPTL
    3.1 Inductive Method of Complete Normal Form
    3.2 Definition of Complete Normal Graph
    3.3 Upper bound of complexity for satisfiability of PPTL
    3.4 Summary
4 Stutter-invariant PPTL
    4.1 Motivation of Introducing Stutter-invariance in PPTL
    4.2 Stutter-Invariance of PPTL
        4.2.1 Stutter-invariance
        4.2.2 Stutter-invariant PPTL(PPTL_(st))
        4.2.3 Complexity of Determining Stutter-invariance
    4.3 Case Study of Compositional Verification in PPTL_(st)
    4.4 Partial-order Model-checking Using PPTL_(st) Specification
    4.5 Compositional Verification of Automatic Gas Station
    4.6 Summary
5 Russian Cards Protocols
    5.1 Russian Cards Problem
        5.1.1 Russian Cards problem
        5.1.2 What is a Safe Communication?
    5.2 Generalization of Russian Cards Problem
        5.2.1 Picking Rule
            5.2.1.1 Construction of B~k in Row Case
            5.2.1.2 Construction of B~k in Column Case
        5.2.2 Deleting Rule
        5.2.3 Safety Proof for R_((n)) in Row Case
        5.2.4 Safety Proof for R_((n)) in Column Case
    5.3 Example
        5.3.1 R_((5)) in Row Case
    5.4 Summary
6 Verifying Russian Cards Protocol with PPTL_(st)
    6.1 Modeling Russian Cards Protocol R_((3))
        6.1.1 The definition of the data structures and initial work
        6.1.2 The definition of honest processes and an intruder
        6.1.3 Safety property specified in PPTL_(st)
        6.1.4 Correspondence of automaton and Never Claim
        6.1.5 Partial-order model checking R_((3))
    6.2 Verification of R_((4)) and R_((5))
    6.3 Summary
7 Conclusion and Future Work
Acknowledgements
References
Publications



本文编号：3180869