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’结构的等价的索引集表达式。