Modeling and verification of mobile systems

This paper describes an approach for modeling and verification of mobile systems. Mobile systems are multi-threaded programs that are characterized by 1) the explicit notion of locations (e.g., sites where they run), 2) the ability to create and execute (possibly infinite) threads at multiple locations (e.g., sites), and 3) the capability to withstand network failures. We give formal semantics to mobile systems as Labeled Kripke Structures (LKSs), which encapsulate the notion of location and unbounded thread creation. This notation allows for the modeling of both data and communication structures of the multi-threaded systems and, thus, outperforms the traditional process algebra approach which captures only the communication behavior. We describe how mobile programs can be exhaustively analyzed by using model checking techniques. The LSKs are readily usable from within the SATABS toolset. SATABS implements the SAT-based counterexample-guided abstraction refinement framework (CEGAR for short) for ANSI-C programs, and supports verification of multi-threaded programs with unbounded thread creation. We are currently developing a front-end to SATABS that allows for languages with explicit location features, such as mobile agents. To the best of our knowledge, this is the first approach that allows modeling and verification of the full spectrum of mobile systems properties.