Research On Key Issues Of Mobile Ambients And Model Checking Applications

In the last ten years, ambient-based process calculus attracts much attention in the researching on formal-modeling theory of mobile computation systems, and many interesting theoretical works are presented. However, all those models are theoretical and too abstract to applications. So many issues should be studied on their implementation such as constructing fundamental programming and modeling languages, Computer-Aided or automatic tools for model-checking and so on. To solve problems above, research works have been done in this dissertation on the follows: ambient-based extended calculus for formal-modeling application of mobile computation systems, ambient-based spatial logic, partial-order reduction algorithm of model-checking in ambient-based spatial logic against ambient-based calculus, and the implementation framework of ambient-based model-checking system. The contributions of this dissertation include:1. An ambient-based extended calculus, named Applied Ambients Calculus( for short, Applied-AC), is proposed. This calculus is provided the semantic of IF-THEN-ELSE which is the fundamental property for implementation-oriented programming and modeling languages of mobile computation systems, and finite-states characters of the calculus which are required for verification of spatial properties of mobile computation systems. Firstly, processes constructed by IF-THEN-ELSE, in which is the first time in ambient-based calculus, and parametric recursion processes are added in this calculus, and the semantics of IF-THEN-ELSE process are interpreted by a special normalization operation, thus semantic interpretations of spatial logic for model checking is simplified. Secondly, properties of finite-control of processes are considered in this calculus, which is a type-system is designed for guaranteeing the finite-state properties while processes executing on conditions of equivalent relations induced by structure congruence semantics. In addition, the translation methods from finite-control processes of Applied-AC to finite-control processes of Pi-calculus are given. So the type-systems designed for Applied-AC processes and the methods of translating finite-control processes of Applied-AC to finite-control processes of Pi-calculus are applicative to other ambient-based extended calculus which includes co-action primitives.2. A decidable ambient-based spatial logic, named Applied Ambient Logic (for short, Applied-AL) is proposed, which is consists of spatial modal connectives and behavioral modal connectives. In ambient logic, the composition adjunct is very expressive, which makes it possible to observe behavioral properties of processes, however it is proved that model-checking of logics with composition adjunct is undecidable. In Applied-AL, behavioral modal connectives are added which can specify behavioral properties of processes directly, and logic semantics and model-checking algorithm against Applied-AC are also given. Furthermore, relations between logic equivalences and structural congruence under Applied-AC semantics are also presented, and shows that logic equivalences can more abstractly observes behavioral properties of Applied-AC processes compares to structural congruence.3. In order to alleviate state-space explosion problem, Partial-order reduction algorithm of model-checking in ambient-based logic and ambient-based calculus is proposed. Firstly, challenges of applying partial-order reduction method to model-checking in ambient-based logic and ambient-based calculus, and properties of partially confluent reduction and factors in preventing partially confluent reduction in Applied-AC processes are investigated. Thus sufficient conditions are given to determine whether a reduction is partially confluent or not. Secondly, relations between spatial properties specified by spatial formulas and the changes of spatial properties when a partially confluent reduction of processes be executed is investigated, and thus sufficient conditions to determine whether the behavior of processes cannot be observed by spatial formulas while a partially confluent reduction performs is presented. Finally, the method and implemental algorithm are given to determine whether partial- order reduction method can be applied to verify properties of logic formulas in model-checking Experiments shows the algorithm is effective and efficient to alleviate state-space explosion problem especially to deadlock and safety properties checking.4. The key data structures and algorithms for developing Computer-aided software or tools for model checking and a prototype are brought out at last. To develop a spatial logic model checking system, it is challenging to design the data structures and algorithms to determine whether a process is structural congruent with another. Because of introducing of IF-THEN-ELSE process and parametric recursion process in Applied-AC, the executing of a recursion process is not the repeating of instance of the same process, and thus data structure of processes in model checking system should not directly adopt tree-like structure. In this algorithm, each Applied-AC process in model checker should be translated into process-equations equivalently; therefore checking structure congruent relation between two processes is translated into checking structure equivalent relation between two corresponding process-equations. The prototype of model checking system has been developed, and correctness of the algorithm is proved by experiments.To summarise up, several key problems in applying ambient-based calculus to formal-modeling of mobile computation systems have been studied in this dissertation. Contributions listed above are helpful for enhancing the reliability of formal-modeling for mobile computation systems in both theory and practice.