Constraint Solving And Formal Verification With MSVL

MSVL is a Modeling, Simulation and Verification Language for concurrent and reactive systems. It is an executable subset of the interval-based temporal logic Projection Tem-poral Logic (PTL) and includes abundant data types, function calls, and synchronous and asynchronous communication mechanisms. As a result, MSVL is practical and has been successfully used in specifying and verifying many applications, such as C programs, Verilog/VHDL programs, virtual memory management, and multi-core computation.In practice, many applications usually involve constraints, such as scheduling, planning and resource allocation, which are generally called Constraint Satisfaction Problems (CSPs). However, MSVL may not handle these problems in a suitable way due to the lack of constraints. Therefore, to manage those fields with constraints, this thesis is motivated to extend MSVL with linear constraints. Further, for a specific kind of CSPs, such as the coins problem, the existing techniques might not be able to efficiently deal with them especially when the involved variables and constraints are numerous. Therefore, to solve this specific sort of CSPs, this thesis proposes an effective approach with the extended MSVL.Since distributed systems are inherently concurrent and asynchronous, it is a challenge to verify distributed systems. The technique of theorem proving can cope with both finite and infinite systems and is appropriate for guaranteeing the correctness of distributed systems. At present, an axiomatic system of MSVL has been established. Nevertheless, it lacks mecha-nisms to manage asynchronous communication, which makes it cannot treat with distributed systems. Hence, to verify distributed systems with MSVL in a deductive way, this thesis is also motivated to extend the axiomatic system of MSVL with new axioms for asynchronous communication. During the verification with MSVL, Propositional PTL (PPTL) is usually employed as the specification language. Due to the significance of fixed-points in formal verification, in order to build a theoretical foundation for the verification with MSVL and PPTL that is by computing fixed-points, this thesis also investigates some fixed-point issues in PPTL.The main contributions of this dissertation are summarized as follows:Firstly, linear constraints over integers are introduced into MSVL. To this end, linear constraint statements are defined and some related issues are discussed. Then to formally capture the intended behaviors of linear constraints in MSVL, the operational semantics of linear constraints is presented, which consists of semantic equivalence rules and transition rules within a state. Particularly, semantic equivalence rules transform linear constraint statements into equivalent forms while transition rules within a state deal with constraint solving and replacement as well as capture the minimal models of programs in the extended MSVL. Further, the soundness of the operational semantics and some interesting properties are proved.Secondly, two common features of the specific kind of CSPs are characterized. In general, such a problem is made up of a series of smaller sub-problems and sub-problems share a similar pattern with equal size and similar linear constraints. With the extended MSVL, each sub-problem is solved in a single state and the original problem is managed over an interval with a simple combination of sub-problems. In this way, similar variables can be reused between different sub-problems, which greatly reduces the number of variables and results in faster solving time. Further, to solve each sub-problem in a state, three types of external solvers are invoked, namely Satisfiability Modulo Theory solvers, Mixed Integer Programming solvers and Constraint Programming solvers. For each sort of solvers, a solving procedure for calling and a translation algorithm from state linear constraints to its standard input language are given. Moreover, to facilitate using the extended MSVL, the tool MSV is modified and all the solving procedures are implemented within it as plug-ins. In addition, the classical coins problem is solved to illustrate how our method works for this class of CSPs. The results reveal that our technique performs well for these problems.Thirdly, some state axioms about message passing are formalized within the axiomatic system of MSVL, which can deduce asynchronous communication commands into their normal forms. Then the soundness and completeness of state axioms are proved. Further, to demonstrate how to use the extended axiomatic system of MSVL, the well-known Ricart-Agrawala (RA) algorithm is employed, which is a distributed mutual exclusion algorithm and has an infinite state space. To do this, the RA algorithm is modeled with MSVL, its desired properties are specified with PPTL and then an instance of the RA algorithm is verified with respect to the first-come-first-served property.Fourthly, some fixed-point issues in PPTL are studied by means of index set expressions and some well-formed index set expressions are identified. To this end, first two sorts of index set expressions Vi∈N0 OiP and Vi∈N0,Pi are proved to be equivalent to PPTL formulas □P and P* respectively, which leads to the fact that they are well-formed. Further, the least and greatest fixed-points of an abstract equation X= Q∨P∧ OX are explored by the index set expression Vi∈0 Pi∧○iQ. Then a technique for determining the exact solution of a concrete equation is provided. With this method, three well-formed index set expressions are obtained. Besides, some fixed-point issues in Propositional Linear Temporal Logic (PLTL) are discussed using the approach of index set expressions. In particular, constructs’U’(strong until) and ’W’ (weak until) of PLTL are equivalently represented with index set expressions.