本文提出了打結(jié)不變的命題投影時(shí)序邏輯,介紹了基于該邏輯的模型檢測方法,并采用該方法驗(yàn)證了無條件安全通信協(xié)議。命題投影時(shí)序邏輯（PPTL）可表達(dá)所有ω-正則式其表達(dá)能力強(qiáng)于其他線性命題時(shí)序邏輯（如PTLL）,此外作為性質(zhì)描述語言,其中的projection和chop算子使得性質(zhì)定義更為靈活,因此PPTL適用于有窮狀態(tài)并發(fā)系統(tǒng)的描述和驗(yàn)證。基于PPTL的模型檢測方法近年來被提出,然而其作為一種形式化驗(yàn)證方法同樣要面臨狀態(tài)爆炸問題。為此,本文定義了PPTL的打結(jié)不變子邏輯（記作PPTLst）,證明了PPTLst可表達(dá)所有PPTL可表達(dá)的打結(jié)不變性質(zhì)。由于PPTLst定義的性質(zhì)對系統(tǒng)中打結(jié)等價(jià)的行為不做區(qū)別,所以在偏序規(guī)約驗(yàn)證中,針對打結(jié)等價(jià)類只需驗(yàn)證其中的一個(gè)行為而不必驗(yàn)證等價(jià)類中的所有行為。因此支持PPTLst的偏序歸約技術(shù)可避免遍歷整個(gè)系統(tǒng)狀態(tài)空間�；谠撍枷氡疚膶�(shí)現(xiàn)了支持基于PPTLst偏序規(guī)約的模型檢測器。此外,PPTLst還可作為性質(zhì)描述語言用于組合驗(yàn)證。其包含的projection和chop算子允許將性質(zhì)定義在系統(tǒng)路徑中受關(guān)注的狀態(tài)上,并且由這些狀態(tài)構(gòu)成的抽象路徑與原路徑打結(jié)等價(jià)... 

【文章來源】：西安電子科技大學(xué)陜西省 211工程院校 教育部直屬院校

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

【學(xué)位級別】：博士

【文章目錄】：
摘要
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