發(fā)布時間：2017-07-26 21:38

  本文關(guān)鍵詞：MSVL語言的約束求解與形式驗證

  更多相關(guān)文章： 時序邏輯程序設(shè)計 分布式系統(tǒng) 定理證明 線性約束 不動點

【摘要】：MSVL是一種用于并發(fā)系統(tǒng)和反應(yīng)式系統(tǒng)的建模、仿真和驗證語言。它是投影時序邏輯(Projection Temporal Logic)的可執(zhí)行子集,包含了豐富的數(shù)據(jù)類型、函數(shù)調(diào)用以及同步和異步通信機制,具有實用性,已經(jīng)被成功地用于許多領(lǐng)域的驗證中,例如C程序、Verilog/VHDL程序、虛擬內(nèi)存管理以及多核并行計算等。實際中有許多應(yīng)用包含了約束,如調(diào)度、規(guī)劃和資源分配等。這些問題通常被稱作約束可滿足性問題(Constraint Satisfaction Problems).,現(xiàn)有的MSVL語言中缺少約束結(jié)構(gòu),不能處理這些問題。因此,為了使得MSVL能夠求解這些問題,本文在MSVL中擴展了線性約束。另外,對于一類特殊的約束可滿足性問題,如硬問題,當(dāng)涉及的變量和約束個數(shù)很多時,現(xiàn)有的方法求解效率不高。因此,為了有效求解這類約束可滿足性問題,本文提出了一種使用擴展的MSVL語言進行求解的方法。分布式系統(tǒng)固有的并發(fā)性和異步性使得分布式系統(tǒng)的驗證已經(jīng)成為一個挑戰(zhàn)。定理證明方法既能夠處理有窮狀態(tài)系統(tǒng),又能夠處理無窮狀態(tài)系統(tǒng),適合于保障分布式系統(tǒng)的正確性。然而,現(xiàn)有的MSVL語言的公理系統(tǒng)中缺少異步通信機制,不能驗證分布式系統(tǒng)。因此,本文擴展了MSVL的公理系統(tǒng),增加了用于異步通信的公理。在MSVL的驗證中,通常使用命題投影時序邏輯(Propositional Projection Temporal Logic, PPTL)作為性質(zhì)描述語言。鑒于不動點在形式化驗證中的重要作用,為了建立MSVL的基于不動點驗證的理論基礎(chǔ),本文也研究了PPTL的不動點問題。PPTL本文的主要貢獻如下：本文在中引入了整數(shù)域上的線性約束。首先定義了線性約束語句并討論了MSVL相關(guān)問題。為了嚴(yán)格地捕獲中線性約束的行為,給出了線性約束的操作語義。MSVL該操作語義由語義等價規(guī)則和狀態(tài)上的遷移規(guī)則組成。其中,語義等價規(guī)則能夠?qū)⒕�性約束化簡為等價的形式,而狀態(tài)上的遷移規(guī)則既能夠處理約束求解和變量代替又能夠捕獲最小模型語義。同時,證明了操作語義的可靠性和一些其它性質(zhì)。本文描述了一類約束可滿足性問題的兩個特征,即由一系列規(guī)模更小的子問題組成,各個子問題的規(guī)模相同且具有相似的線性約束。對于這類問題,使用擴展的在每個狀態(tài)上求解子問題,從而在整個區(qū)間上求解原始問題。不同的MSVL子問題之間可以重復(fù)利用相同變量,因而減少了變量的個數(shù),提高了求解效率。為了在一個狀態(tài)上求解子問題,調(diào)用了三種外部求解器,分別是可滿足性模理論求解器,混合整數(shù)規(guī)劃((Satisfiability Modulo Theory)求解器Mixed Integer Programming)和約束規(guī)劃(求解器。對于每種求解器,給出了調(diào)用算法和用于Constraint Programming)將狀態(tài)線性約束轉(zhuǎn)換為其標(biāo)準(zhǔn)輸入語言的轉(zhuǎn)換算法。接著,修改了工具MSV并實現(xiàn)了上述所有的算法以便于使用擴展的語言。最后,硬幣問題的實例說明了使用擴MSVL展的語言求解這類問題的可行性和有效性。MSVL本文在的公理系統(tǒng)中定義了用于異步消息傳遞的狀態(tài)公理,這些公理可以MSVL將異步通信命令推演為范式。證明了狀態(tài)公理的可靠性和完備性。為了展示的MSVL擴展公理系統(tǒng)的切實可行性,驗證了著名的Ricart-Agrawala(RA)算法。該算法是經(jīng)典的分布式進程互斥算法,具有無窮狀態(tài)空間。首先使用MSVL語言建模RA算法,然后使用PPTL描述RA算法的期望性質(zhì),最后驗證了一個實例的先來先服務(wù)性質(zhì)。本文使用索引集表達式(index set expression)研究了PPTL的不動點問題,并且給出了一些良定的索引集表達式。首先給出了兩個良定的索引集表達式Vi∈N0 OiP和Vi∈N0 Pi,并證明了它們分別等價于PPTL公式口P和P*。接著,使用索引集表達式Vi∈N0 P(i)∧OiQ研究了抽象方程X≡Q∨P∧OX的最小不動點和最大不動點。同時,提出了一種確定具體方程的精確解的方法。應(yīng)用該方法,得到了三個良定的索引集表達式。最后,使用索引集表達式研究了命題線性時序邏輯(Propositional Linear Temporal Logic,PLTL)的不動點問題。特別地,給出了PLTL中‘U’和‘W’結(jié)構(gòu)的等價的索引集表達式。
【關(guān)鍵詞】：時序邏輯程序設(shè)計 分布式系統(tǒng) 定理證明 線性約束 不動點
【學(xué)位授予單位】：西安電子科技大學(xué)
【學(xué)位級別】：博士
【學(xué)位授予年份】：2015
【分類號】：TP312.1
【目錄】：

• 摘要5-7
• ABSTRACT7-12
• List of Abbreviations12-17
• Chapter 1 Introduction17-29
• 1.1 Formal Verification17-19
• 1.1.1 Model Checking18
• 1.1.2 Theorem Proving18-19
• 1.2 Temporal Logic and Temporal Logic Programming19-23
• 1.2.1 Temporal Logic19-21
• 1.2.2 Temporal Logic Programming21-23
• 1.3 Constraint Solving23-24
• 1.4 Motivation and Contributions24-27
• 1.5 The Organization of the Thesis27-29
• Chapter 2 MSVL and the Underlying Logic29-41
• 2.1 Projection Temporal Logic29-35
• 2.1.1 Syntax29-30
• 2.1.2 Semantics30-31
• 2.1.3 Derived Formulas31-33
• 2.1.4 Precedence Rules33
• 2.1.5 Replacement33-34
• 2.1.6 Logical Laws34
• 2.1.7 Propositional Projection Temporal Logic34-35
• 2.2 MSVL35-40
• 2.2.1 Expressions and Statements35-38
• 2.2.2 Normal Form38-39
• 2.2.3 Minimal Model Semantics of MSVL39-40
• 2.3 Conclusion40-41
• Chapter 3 Integration of Linear Constraints with MSVL41-65
• 3.1 Linear Constraints in MSVL41-45
• 3.1.1 Linear Constraint Statements41-43
• 3.1.2 Derived Statements43
• 3.1.3 Semi-Normal Form43-45
• 3.2 Two Issues45-46
• 3.2.1 Underlying Store45
• 3.2.2 How to Determine Current Values of Variables45-46
• 3.3 Operational Semantics46-53
• 3.3.1 Operational Semantics of MSVL47-49
• 3.3.2 Operational Semantics of Linear Constraints49-53
• 3.4 Soundness of the Operational Semantics53-58
• 3.5 Applications58-61
• 3.5.1 Truck Packing Problem58-59
• 3.5.2 Production Scheduling Problem59-61
• 3.6 Related Work61-63
• 3.7 Conclusion63-65
• Chapter 4 Solving a Specific Kind of CSPs with MSVL65-85
• 4.1 Features of a Specific Kind of CSPs65-67
• 4.2 Invoking of External Solvers67-78
• 4.2.1 Solving Constraints with SMT Solvers68-72
• 4.2.2 Solving Constraints with MIP Solvers72-76
• 4.2.3 Solving Constraints with CP Solvers76-78
• 4.3 Embedding Linear Constraints into MSV78-81
• 4.4 An Application:the Coins Problem81-84
• 4.4.1 Modeling and Solving with the Extended MSVL81-82
• 4.4.2 Comparison with ECL~iPS~e82-84
• 4.5 Conclusion84-85
• Chapter 5 Verification of Distributed Systems with MSVL85-113
• 5.1 Axiomatic Semantics of MSVL85-89
• 5.2 Asynchronous Communication Commands89-90
• 5.3 Asynchronous Communication Axioms90-95
• 5.3.1 State Axioms for Asynchronous Communication90-94
• 5.3.2 Derived Theorems94-95
• 5.4 Soundness and Completeness95-100
• 5.5 An Application:Ricart-Agrawala Algorithm100-110
• 5.5.1 Description100-101
• 5.5.2 Modeling101-102
• 5.5.3 Properties102-106
• 5.5.4 Verification106-110
• 5.6 Related Work110-111
• 5.7 Conclusion111-113
• Chapter 6 Some Fixed-point Issues in PPTL113-137
• 6.1 Two Kinds of Index Set Expressions113-118
• 6.2 Fixed-points of Equation X≡Q ∨P∧○X118-126
• 6.3 Some Well-formed Instances126-131
• 6.4 Fixed-point Issues in Propositional Linear Temporal Logic131-135
• 6.4.1 Syntax and Semantics of PLTL131-132
• 6.4.2 Fixed-point Issues of PLTL132-133
• 6.4.3 A Transformation from PLTL to PPTL133-135
• 6.5 Conclusion135-137
• Chapter 7 Conclusions and Future Works137-141
• 7.1 Conclusions137-140
• 7.2 Future Works140-141
• REFERENCES141-149
• ACKNOWLEDGEMENTS149-151
• BIOGRAPHY151-153
• 1. Personal Profile151
• 2. Educational Background151
• 3. Research Achievement151-153
• APPENDIX153-161

【相似文獻】

中國期刊全文數(shù)據(jù)庫 前3條

1 朱壽國;;廣義混合平衡問題和不動點問題的公共元的混雜算法[J];成都信息工程學(xué)院學(xué)報;2011年04期

2 王天yN;文鈞屹;張絲雨;何秉航;羅宏文;;基于不動點算法的LLT去噪模型[J];吉林大學(xué)學(xué)報(理學(xué)版);2014年04期

3 ;[J];;年期

中國重要會議論文全文數(shù)據(jù)庫 前1條

1 郭秀敏;王國俊;;關(guān)于描述邏輯中不動點語義的討論[A];第六屆中國不確定系統(tǒng)年會論文集[C];2008年

中國博士學(xué)位論文全文數(shù)據(jù)庫 前3條

1 馬倩;MSVL語言的約束求解與形式驗證[D];西安電子科技大學(xué);2015年

2 龍瓏;廣義量子操作不動點問題的研究[D];浙江大學(xué);2011年

3 胡慧英;幾類廣義平衡問題的不動點迭代法[D];上海師范大學(xué);2012年

中國碩士學(xué)位論文全文數(shù)據(jù)庫 前10條

1 劉超;關(guān)于不動點問題的研究[D];天津理工大學(xué);2015年

2 馬苑芳;分裂等式不動點問題的研究及應(yīng)用[D];云南財經(jīng)大學(xué);2015年

3 李卓識;不動點問題的組合同倫算法與復(fù)雜性分析[D];長春工業(yè)大學(xué);2010年

4 劉斌斌;兩類非線性算子的不動點與固有值問題[D];江西師范大學(xué);2004年

5 羅率兵;抽象空間中的不動點問題[D];中國科學(xué)技術(shù)大學(xué);2009年

6 王燕;平衡問題的求解算法初探[D];重慶師范大學(xué);2009年

7 王云亮;平衡問題的例外簇[D];廣西師范大學(xué);2012年

8 郭筱;Hilbert空間中的不動點問題[D];西南大學(xué);2012年

9 孟繁英;非線性算子不動點問題的迭代逼近[D];上海師范大學(xué);2013年

10 左平;關(guān)于擬變分包含和廣義混合平衡的不動點問題的一些研究[D];四川師范大學(xué);2011年

，

本文編號：578505