Research On Model Checking Algorithms Of Ambients Calculi Systems

As an important automatically formal verification technology, model checking has been extensively studied, achieving plentiful fruits and has been applied to diversified fields. The academic world and industrial community are keen on model checking techniques.The base idea of model checking involves that a state transition system, said M , which is used to describe the structures and behaviors of some system, and a modal logic formula, saidψ, which is used to state a property that the system should have. So the problem"Whether this system has the desired property ?"is converted to a mathematical problem, that is"Whether the state transition system M is a model of the formulaψ?".So, we can see that research on model checking primarily focus on two aspects: one is modeling systems under test; the other is using some methods to describe properties correctly and efficiently. In this paper, the target system is Ambient Calculus, which is used to model the computation patterns on WAN and the Internet. The method we used to describe properties of the system is spatial logic, combined with temporal logic, both of which belong to modal logic. We conduct a study from two parts of structural properties of the processes and reduction actions of them. The major work done in this paper is as follows:(1) Firstly we study three calculi of the Ambient Calculus: Mobile Ambients, Safe Ambients and Boxed Ambients. Based on the existing relevant research, we make a lengthwise analysis and comparison of the three systems and also give some typical examples correspondingly.(2) Based on analysis of the above Calculi, we present them reduction-oriented spatial logic respectively. On the one hand, the static parts of the logic describes structural properties of the processes, not only including traditional structural operators, but also bringing in some new operators to describe prefixed actions of the processes. On the other hand, the dynamic parts give reduction actions, that is, processes satisfy some properties after doing one step ofτ-action. We don't adopt behavioral semantics, so it's unnecessary to think about other actions such as in ,out , etc.(3) We provide data structure representations for both the systems and logics. And then decide whether the model has the properties stated by our logics based on the model checking principles. This paper gives the model checking algorithms and verify the correctness of them.