ERCIM News No.36 - January 1999

Modelling Mobile Applications

by Stefania Gnesi and Laura Semini

---

There has been growing interest in wide-area distributed applications in recent years. A key concept for structuring such applications is represented by mobile agents, units of executing code that can migrate between sites.

At IEI-CNR we are currently working in the area of mobile systems. We have focused on those mobile applications that are composed of a set of components migrating among distinguished sites. In these systems there is a dynamically changing connection topology among the system sub-components. Some typical examples are: the cellular telephone system, where a Mobile Station (the telephone), moving through different geographical areas, interacts with a cell that is able to manage the communication with the final receiver; and satellite communication systems.

Most languages used to describe applications in a distributed setting provide an abstraction away from the underlying architecture, ie, from the way the application components are distributed over a network and from the way that the connections among the nodes of the network are realized. The advantages of this abstraction are independence from all physical details that are not relevant at the application level, and better reasoning on the program properties.

In particular, distributed, non-mobile languages can provide constructs, usually based on shared memory or on message passing paradigms, for the synchronous composition of the components of an application. These constructs completely abstract away from the component allocations and from the way synchronous communication is implemented. In both cases, everything should operate smoothly, ie, the behaviour of the system will be correct with respect to the definition of the semantics, since it is reasonable to hypothesise that, in general, communication failures will not occur in a distributed, non-mobile network. In fact, it can be presumed that a run-time support based on a non-mobile network will hide the few communication failures that can occur in these networks.

On the contrary, in a mobile architecture, typically based on wireless communications, the same hypothesis no longer holds and no run-time system can hide a lack of connection which can last for hours.

Two solutions can be adopted to address this problem:

1. The definition of languages to model mobile applications that include a synchronous composition construct. The drawback in this case is that, at the language level, the presence or lack of physical connection among the subsystems must be dealt with; connections cannot be assumed to be always on.

2. No synchronous communication is permitted among distinguished mobile entities, and applications are described using asynchronous languages. Ignoring synchrony, it is possible to describe most applications without mentioning any notion of connection, location, or channel, ie, keeping the description completely abstract with respect to the underlying architecture.

We have explored this solution, proposing a high level programming language based on asynchronous message passing. The language frees the developers of a mobile application from considering low level issues, and leads to descriptions that are highly readable and completely abstract from the physical architecture of the underlying net. To make our proposal effective, we have shown how to implement the language communication primitives when the underlying architecture is a mobile one.

Together with modelling issues, it is also important to define methods and tools for the formal verification of mobile systems in order to guarantee their correct behaviour. Some work has been done recently in this respect and a formal verification environment, named HAL, has been defined to check the satisfiability of safety and liveness properties of mobile systems modelled as process calculi terms. HAL was used in the formal verification of the core of the handover protocol for the GSM Public Land Mobile Network proposed by the European Telecommunication Standards Institute. The same environment has been used to verify the correctness of an implementation of the GSM Short Message Service, a service that provides an electronic postcard service working over GSM, enabling the sending and receiving of short text messages among GSM phone users.

Please contact:

Stefania Gnesi - IEI-CNR
Tel: +39 050 593 489
E-mail: gnesi@iei.pi.cnr.it