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
