MSVL语言的约束求解与形式验证

发布时间：2017-07-26 21:38

  本文关键词：MSVL语言的约束求解与形式验证

  更多相关文章： 时序逻辑程序设计 分布式系统 定理证明 线性约束 不动点

【摘要】：MSVL是一种用于并发系统和反应式系统的建模、仿真和验证语言。它是投影时序逻辑(Projection Temporal Logic)的可执行子集,包含了丰富的数据类型、函数调用以及同步和异步通信机制,具有实用性,已经被成功地用于许多领域的验证中,例如C程序、Verilog/VHDL程序、虚拟内存管理以及多核并行计算等。实际中有许多应用包含了约束,如调度、规划和资源分配等。这些问题通常被称作约束可满足性问题(Constraint Satisfaction Problems).,现有的MSVL语言中缺少约束结构,不能处理这些问题。因此,为了使得MSVL能够求解这些问题,本文在MSVL中扩展了线性约束。另外,对于一类特殊的约束可满足性问题,如硬问题,当涉及的变量和约束个数很多时,现有的方法求解效率不高。因此,为了有效求解这类约束可满足性问题,本文提出了一种使用扩展的MSVL语言进行求解的方法。分布式系统固有的并发性和异步性使得分布式系统的验证已经成为一个挑战。定理证明方法既能够处理有穷状态系统,又能够处理无穷状态系统,适合于保障分布式系统的正确性。然而,现有的MSVL语言的公理系统中缺少异步通信机制,不能验证分布式系统。因此,本文扩展了MSVL的公理系统,增加了用于异步通信的公理。在MSVL的验证中,通常使用命题投影时序逻辑(Propositional Projection Temporal Logic, PPTL)作为性质描述语言。鉴于不动点在形式化验证中的重要作用,为了建立MSVL的基于不动点验证的理论基础,本文也研究了PPTL的不动点问题。PPTL本文的主要贡献如下：本文在中引入了整数域上的线性约束。首先定义了线性约束语句并讨论了MSVL相关问题。为了严格地捕获中线性约束的行为,给出了线性约束的操作语义。MSVL该操作语义由语义等价规则和状态上的迁移规则组成。其中,语义等价规则能够将线性约束化简为等价的形式,而状态上的迁移规则既能够处理约束求解和变量代替又能够捕获最小模型语义。同时,证明了操作语义的可靠性和一些其它性质。本文描述了一类约束可满足性问题的两个特征,即由一系列规模更小的子问题组成,各个子问题的规模相同且具有相似的线性约束。对于这类问题,使用扩展的在每个状态上求解子问题,从而在整个区间上求解原始问题。不同的MSVL子问题之间可以重复利用相同变量,因而减少了变量的个数,提高了求解效率。为了在一个状态上求解子问题,调用了三种外部求解器,分别是可满足性模理论求解器,混合整数规划((Satisfiability Modulo Theory)求解器Mixed Integer Programming)和约束规划(求解器。对于每种求解器,给出了调用算法和用于Constraint Programming)将状态线性约束转换为其标准输入语言的转换算法。接着,修改了工具MSV并实现了上述所有的算法以便于使用扩展的语言。最后,硬币问题的实例说明了使用扩MSVL展的语言求解这类问题的可行性和有效性。MSVL本文在的公理系统中定义了用于异步消息传递的状态公理,这些公理可以MSVL将异步通信命令推演为范式。证明了状态公理的可靠性和完备性。为了展示的MSVL扩展公理系统的切实可行性,验证了著名的Ricart-Agrawala(RA)算法。该算法是经典的分布式进程互斥算法,具有无穷状态空间。首先使用MSVL语言建模RA算法,然后使用PPTL描述RA算法的期望性质,最后验证了一个实例的先来先服务性质。本文使用索引集表达式(index set expression)研究了PPTL的不动点问题,并且给出了一些良定的索引集表达式。首先给出了两个良定的索引集表达式Vi∈N0 OiP和Vi∈N0 Pi,并证明了它们分别等价于PPTL公式口P和P*。接着,使用索引集表达式Vi∈N0 P(i)∧OiQ研究了抽象方程X≡Q∨P∧OX的最小不动点和最大不动点。同时,提出了一种确定具体方程的精确解的方法。应用该方法,得到了三个良定的索引集表达式。最后,使用索引集表达式研究了命题线性时序逻辑(Propositional Linear Temporal Logic,PLTL)的不动点问题。特别地,给出了PLTL中‘U’和‘W’结构的等价的索引集表达式。
【关键词】：时序逻辑程序设计 分布式系统 定理证明 线性约束 不动点
【学位授予单位】：西安电子科技大学
【学位级别】：博士
【学位授予年份】：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

【相似文献】

中国期刊全文数据库 前3条

1 朱寿国;;广义混合平衡问题和不动点问题的公共元的混杂算法[J];成都信息工程学院学报;2011年04期

2 王天yN;文钧屹;张丝雨;何秉航;罗宏文;;基于不动点算法的LLT去噪模型[J];吉林大学学报(理学版);2014年04期

3 ;[J];;年期

中国重要会议论文全文数据库 前1条

1 郭秀敏;王国俊;;关于描述逻辑中不动点语义的讨论[A];第六届中国不确定系统年会论文集[C];2008年

中国博士学位论文全文数据库 前3条

1 马倩;MSVL语言的约束求解与形式验证[D];西安电子科技大学;2015年

2 龙珑;广义量子操作不动点问题的研究[D];浙江大学;2011年

3 胡慧英;几类广义平衡问题的不动点迭代法[D];上海师范大学;2012年

中国硕士学位论文全文数据库 前10条

1 刘超;关于不动点问题的研究[D];天津理工大学;2015年

2 马苑芳;分裂等式不动点问题的研究及应用[D];云南财经大学;2015年

3 李卓识;不动点问题的组合同伦算法与复杂性分析[D];长春工业大学;2010年

4 刘斌斌;两类非线性算子的不动点与固有值问题[D];江西师范大学;2004年

5 罗率兵;抽象空间中的不动点问题[D];中国科学技术大学;2009年

6 王燕;平衡问题的求解算法初探[D];重庆师范大学;2009年

7 王云亮;平衡问题的例外簇[D];广西师范大学;2012年

8 郭筱;Hilbert空间中的不动点问题[D];西南大学;2012年

9 孟繁英;非线性算子不动点问题的迭代逼近[D];上海师范大学;2013年

10 左平;关于拟变分包含和广义混合平衡的不动点问题的一些研究[D];四川师范大学;2011年

，

本文编号：578505