Article Preview
Top1. Introduction
The advent of concurrent and multi-threaded programming has led to the development of complex and highly-evolving interactive systems which concurrently run two or more independent, interactive processes with dynamically evolving structures (Davis, 2000). The introduction of mobile computing introduced a whole new layer of abstraction in these systems – mobility. Systems comprising of mobile agents or mobile systems in general, contain dynamic links which are constantly changing. New links are created on-the-fly, existing links transferred or deleted (Fernandez & Mounier 1992). This dynamics makes the mobile systems much more complex than their counterparts and comparatively difficult to model. Such concurrent mobile systems may be implemented via processes and/or threads which execute in a relatively independent way. However, since they are acting together towards some common goal, they need to communicate and coordinate. The two most common communication techniques in processes and threads are through message passing and shared variables respectively. We try to avoid the shared variables paradigm because it forces the usage of complicated and time-delaying mutual exclusion techniques as multiple processes making assignments to the same shared variable can lead to unpredictable behavior if the assignments are made concurrently. Now, if an unnoticed bug gets introduced in the design of such a system it will propagate into every development stage of the system. Depending on the application design, the entire system might break after its initial deployment. Traditional testing techniques are of limited help here, since test coverage is bound to be only a minute fraction of the possible behaviors of the system. Moreover, bugs in concurrent systems are usually very hard to reproduce and hence hard to understand. Thus, formal verification methods that detect errors, inconsistencies and incompleteness at early development stages will help improve the software development cycle especially at the Testing and Debugging stage.
For a system to be verified, its system specification and its intended behavior have to be described in a precise and formal way. This will allow verifying mathematically, as to whether it is behaving according to the designer’s intensions and to reason about the behavior of the system. One way to formally describe a system is to use process algebra. Process algebras are standard paradigm for describing and analyzing communicating concurrent systems (Milner, 1989). It refers to the algebraic approach of studying concurrent processes. We use algebraic languages for specifying processes and statements about them, and a calculus for verifying the statements. The three main classical algebraic approaches to concurrency are Calculus of Communicating Systems (CCS) (Milner, 1989), Communicating Sequential Processes (CSP) (Hoare, 1985) and Algebra of Communicating Processes (ACP) (Bergstra & Klop, 1985). CCS is one of the first of process calculi and was developed by Robin Milner. It models the pure communication and synchronization aspects of concurrent systems and includes primitives for describing parallel composition, choice between actions and scope restriction.
CSP was introduced in early 1980’s by Hoare (1985). It is a formal language for describing patterns of interaction. As its name suggests, CSP allows a user to describe systems as a number of (parallel) components (processes) that operate independently and communicate with each other solely over well-defined channels. It introduces a process algebra which can be used to describe a process' communications with its environment. In addition, it has been successfully used as the basis for the programming language Occam, and in recent years has been extended into a wider domain, for example to address tasks in hardware co-design. In ACP (Bergstra & Klop, 1985) on the other hand, process algebra was extended with communication to yield its theory. It emphasizes the algebraic aspect: there is an equational theory with a range of semantical models. Also, ACP has a more general communication scheme. However, with the aforementioned process algebras it is difficult to model systems where the structure of communication changes dynamically as these mobile systems contain dynamic links that are constantly changing. These dynamics make the mobile systems much more complex than their counterparts and comparatively difficult to model.