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的不动点问题，并且给出了一些良定的索引集表达式。首先给出了两个良定的索引集表达式∨i∈NO○iP和∨i∈NO Pi,并证明了它们分别等价于PPTL公式□P和P*。接着，使用索引集表达式∨i∈NO P(i)∧○iQ研宄了抽象方程X≡ Q∨P∧○X的最小不动点和最大不动点。同时，提出了一种确定具体方程的精确解的方法。应用该方法，得到了三个良定的索引集表达式。最后，使用索引集表达式研宄了命题线性时序逻辑(Propositional Linear Temporal Logic，PLTL)的不动点问题。特别地，给出了PLTL中‘U’和‘W’结构的等价的索引集表达式。

目录

封面

声明

中文摘要

英文摘要

List of Figures

List of Tables

List of Abbreviations

目录

Chapter 1 Introduction

1.1 Formal Verification

1.2 Temporal Logic and Temporal Logic Programming

1.3 Constraint Solving

1.4 Motivation and Contributions

1.5 The Organization of the Thesis

Chapter 2 MSVL and the Underlying Logic

2.1 Projection Temporal Logic

2.2 MSVL

2.3 Conclusion

Chapter 3 Integration of Linear Constraints with MSVL

3.1 Linear Constraints in MSVL

3.2 Two Issues

3.3 Operational Semantics

3.4 Soundness of the Operational Semantics

3.5 Applications

3.6 Related Work

3.7 Conclusion

Chapter 4 Solving a Specific Kind of CSPs with MSVL

4.1 Features of a Specific Kind of CSPs

4.2 Invoking of External Solvers

4.3 Embedding Linear Constraints into MSV

4.4 An Application: the Coins Problem

4.5 Conclusion

Chapter 5 Verification of Distributed Systems with MSVL

5.1 Axiomatic Semantics of MSVL

5.2 Asynchronous Communication Commands

5.3 Asynchronous Communication Axioms

5.4 Soundness and Completeness

5.5 An Application: Ricart-Agrawala Algorithm

5.6 Related Work

5.7 Conclusion

Chapter 6 Some Fixed-point Issues in PPTL

6.1 Two Kinds of Index Set Expressions

6.2 Fixed-points of Equation X≡Q∨ P∧○X

6.3 Some Well-formed Instances

6.4 Fixed-point Issues in Propositional Linear Temporal Logic

6.5 Conclusion

Chapter 7 Conclusions and Future Works

7.1 Conclusions

7.2 Future Works

参考文献

致谢

BIOGRAPHY

1. Personal Profile

2. Educational Background

3. Research Achievement

APPENDIX