Model Checking Methods For Value-Passing And Mobile Processes

Concurrency theory studies the phenomenon of concurrent computation in which many distributed computing agents participate in a common computation task and cooperate with each other by exchanging message (Communication). Since 1960's, a number of concurrency theory have been proposed and extensively studied, including Petri nets, process algebra, modal logic etc. Among them, CCS (Calculus of Communication System) and its variations is one of the most influenced.Model checking is an automatic technique for analysing and verifying finite state concurrent systems. Its basic idea is to model a concurrent system as a state transition graph S and to describe system property as a modal/temporal logic formula φ, then the problem "if system has the desired property" becomes the mathmatical problem "whether S satisfies φ", denoted as S φ. For finite state model S, this is decidable. Generally speaking, model checking enjoys two remarkable virtues: It is fully automatic and when the system fails to satify a desired property, a diagnostic message can be generated which demonstrates a behavior violating the property.The content of the thesis cosists of two parts: model checking methods for value-passing systems and for mobile systems, both based on first-order extensions of μ—calculus.The first part concerns value-passing CCS. Firstly, the consistency between the predicate μ—calculi and modal graphs is studied. To make predicate μ—calculus formulae easier manipulated by computer programs, modal graphs are proposed as a graphical formulation of predicate μ—calculus. With the introduction of predicate equation systems, the semantic consistency between the logic and modal graphs is established. Moreover, a better algorithm is proposed to transform a predicate μ—calculi formula to a modal graph. Secondly, a method is put forward to generate useful diagnostic information in model checking value-passing processes. Two diagnostic forms, proof graphs and witnesses are defined. Correspondingly, their construction algorithms are proposed. The method has been implemented as part of our model checker and tested by several examples. Thirdly, a patial order reduction method for value-passing CCS is proposed to cope with the state-explosion problem. With studies on the relationship between the weak predicate μ—calculi and the weak bisimulation of STGA, it is prove that in value-passing CCS, two weak bisimular processes satisfy the same weak predicate μ—calculus formulae, moreover for finite-image systems reverse statement is also true. The inert transitions in STGAs are defined and it is proved that two states before and after an inert transitionare weak bisimular. Theofore, they satisfy the same weak predicate —calculi formulae. Based on the above results, we propose apatrial order reduction method for value-passing CCS and it is now interiged in our tool.The second part concerns mobile ambients, a process calculus for mobile systems. We implement a model checker for finite-control mobile ambients. First, we propose a de bruijn notation for finite-control mobile ambients and moreover with its normal form, a lower-layer notation for the processes are contructed. The structure congruence realtion and reduction relation for the processes are both implemented. Based on the above results, we implement a model checking algorithm for finite-control mobile ambients which can deal with ambient logic with fixed-point opertors. It is the first such tool for model checking mobile ambients.