Modeling, Verification And Testing With The Extended π-calculus

Time-dependent concurrent mobile systems are a kind of computing system characterized by concurrency, mobility, time dependence and heterogeneity. For such systems, particularly safety-critical systems, e.g., mobile payment systems, mobile communication systems, traffic control systems, their failure and collapse may cause significant loss. Therefore, quality characteristics of time-dependent concurrent systems, such as correctness and security, have widely received attention. An effective method, which can reduce the design mistakes and ensure the quality of these systems, is using formal methods for modeling, verification and testing of time-dependent systems.Process algebras are typical formal methods and useful in the specification and verification of concurrent systems. Lots of variations of process algebras are proposed for different purposes. E.g., -calculus is given for expressing mobility. Recently, with the development of new network computing technologies, -calculus has been widely used in practice to ensure the correctness of the systems with dynamic properties. However, the time duration of an action and the residence time of a system at a state are not taken into account. Thus,-calculus is not convenient for modeling, verification and testing of time-dependent systems.We are motivated to extend -calculus so that time-dependent systems can be modeled and verified. In this thesis, an extended -calculus added by time-dependent characteristics is investigated. Based on this, a method using extended -calculus for modeling and reasoning about time-dependent concurrent mobile systems is presented. Further, to verify systems modeled by the extended -calculus automatically, a structure transformation from p-Ï€ to MSVL is given. In addition, to test systems modeled by the extended -calculus, a test case generation method based on the extended -calculus is proposed. The main contributions of the dissertation could be outlined as follows:(1) An extended -calculus with interval action prefixes is presented and called p-Ï€. Firstly,the syntax and operational semantics of p-Ï€ is defined. And then the algebraic and timedependent properties are given and proved. Based on these, how to model time-dependent behaviors by p-Ï€ is demonstrated. In addition, a case study is given to illustrate how p-Ï€ is used in practice and the effect of these properties.(2) A method based on the extended -calculus p-Ï€ is presented to formally model and reason about time-dependent concurrent mobile systems. Both the interval action prefixes and the instantaneous action prefixes are employed to respectively describe the time-dependent behaviors and communications of systems. Operators are used to composite sub-processes,and then operational rules are utilized to construct a time-dependent labeled transition system and acceptable executive paths of the system. The properties of the system are then deduced by means of the transition system and the acceptable executive paths. Experimental analyses on a mobile vehicle control system(MVCS) show that the approach effectively models and reasons about time-dependent concurrent mobile systems and improves the reliability of time-dependent concurrent mobile systems.(3) A structural transformation approach from p-Ï€ processes to MSVL programs is proposed.To this end, channel and communication primitives are firstly defined in MSVL. Further,based on these definitions, a mapping function which transforms bounded p-Ï€ processes into MSVL programs is formalized and the consistency of the communications used by the two formalisms is proved. Moreover, the soundness of the transformation is proved by the bisimulation over the TDLTS of a p-Ï€ process and the set of reduction configurations of an MSVL program. By the transformation, p-Ï€ can provide a mechanism to model,simulate and verify concurrent time-dependent systems by means of the techniques of MSVL.(4) A method based on the extended -calculus p-Ï€ is presented to generate test case by considering the questions in testing for time-dependent concurrent mobile systems.It employs p-Ï€ to describe behaviors of time-dependent concurrent mobile systems.Then operational rules are utilized to construct the time-dependent labelled transition system(TDLTS) of the system.By means of TDLTS and use case specification, test case can be generated according to the executable action,path and time constraint coverage criterion.Further, the selection strategies of test case are given. In addition,the verification based on p-Ï€ ensures the correctness of generated test case.