Detail

Mobile Calculi based on Domains

The goal of MIKADO is to construct a new formal programming model, based upon the notion of domain as a computing concept, which supports reliable, distributed mobile computation, and provides the mathematical basis for a secure standard for distributed computing in open systems.

Specifically, MIKADO intends:

to develop new formal models for both the specification and programming of large-scale, highly distributed and mobile systems;
to develop new programming languages features supporting such models, and to study their combination with functional and object-oriented programming;
to develop specification and analysis techniques which can be used to build safer and trustworthy systems, to demonstrate their conformance to the specifications, and to analyse their behaviour;
and to prototype new virtual machine technologies that can be used to implement in a “provably correct” way such models and languages.
The overall goal of the Mikado project is to construct a new formal programming model, based
upon the notion of domain as a computing concept, which supports reliable, highly distributed and
mobile computation, and provides the mathematical basis for a secure standard for distributed
computing in open systems.
The term “global computing” is used to describe a projected scenario in which processors will be
everywhere, e.g. in household devices, in cars, in clothing etc, and in which networks will be
heterogeneous and highly diverse in their capabilities, e.g. high-speed networks, ad-hoc wireless
networks etc. They will be able to communicate and also sense and interact with their environment.
The result is a “massive networked infrastructure composed of highly diverse interconnected objects
that should support the design and use of systems with a predictable and desirable behaviour”1. Such
systems are also typically autonomous, inherently mobile, have configurations that vary over time and
operate on the basis of incomplete information. Furthermore, they are likely to consist of a mixture of
personal and more public devices. The challenge is then to “define and exploit dynamically configured
systems of mobile entities that interact in novel ways with their environment to achieve or control
their computational tasks”1.
Current middleware and programming language technologies are inadequate to meet the challenges
posed by such an environment. In particular, they tend to support a limited range of interactions, have
a limited view of components and objects, fail to properly and uniformly support properties such as
mobility, predictability, security, fault-tolerance, and are not amenable to rigorous investigation for
verification, validation and test purposes. In a global computing environment, characterised by its
openness and its ubiquity, these limitations become real design and construction bottlenecks. In order
to overcome these different limitations, the Mikado project intends to develop new formal models for
global computing. Models with a formal (i.e. mathematical) semantics, should provide a sound basis
for constructing global computing systems which are “sound by construction” and which behave in a
predictable and analysable manner. Indeed, providing quality of service guarantees in such an open
and large-scale context, where “quality of service” refers to broad non-functional properties such as
security, responsiveness, fault-tolerance, real-time, availability, etc, requires sophisticated and
rigorous means of analysis and verification, which only formal models can provide.