Programming Models and Specification of Goals in Distributed Computing.

1.  Distributed systems are closely related to systems having real time
constraints and which need a high degree of safety.

The use of Distributed computing is natural in many classes of
applications: transportation, industrial control, communications, safety
critical systems.  For these applications the percentage of software in the
development cost can be very high , as in telecommunications, but even if
it is small , as in transportation, software is a critical factor, i.e.
malfunctioning software can be catastrophic.
These applications require a high degree of safety, and for them
distributed computing is a mixed blessing:
On the one hand, the  applications themselves lead naturally to distributed
implementations.   Safety schemes are basically based on replication and
distributed computation, "can" provide a gain of speed sometimes.
On the other hand, distributed computation can bring a lot of trouble:
- the possibility of deadlocks;
- transmission time which leads to non-determinism;
- the  need to  have sophisticated algorithms for establishing a global state.
Although it is a banality to say that correctness is both more difficult,
and even more of a necessity, this necessity is increasing with the spread
of software-based industrial products.

2.  Specification of properties is necessary to establish correctness

Correctness of distributed programs is clearly a strategic direction for
research.  Since it is a very broad and general subject, let us focus on a
specific point.

In general the only possible answer to the question "Is my program
correct?" is "yes."  In fact the program does what its instructions tell it
to do (assuming no hardware or compiler error).  A "no" answer can be
produced only if one mentions what "correct" means.  As the works of
logicians show, the expression of the expected properties cannot be in the
same language as the programs themselves.  The expression of needs and
expected properties are to be considered at the specification level.  We
believe that most research done on distributed programs concerns models of
programs, and not the expression of properties.  Distributed objects,
actors PRAM, etc  all have to do with the way instructions (computation or
synchronisation)  are executed.  Semantics for these models  are defined,
some good properties of programs are stated, and then it is shown how to
establish them.  This type of work is essential both for expressing
distributed programs, and for defining what type of properties is needed.
It deals with some steps in the development process, but does not fit well
with the specification steps.

An approach that has proven successful in the centralized case is the
coupling of finite automata with model checking.  The automaton represents
the programming model, and temporal logic the way to express the properties
that have to be checked for the programmers, as well as the users of the
programs .
In fact, this coupling has produced such good results that programming
models like the synchronous approach have been used for systems that are
naturally distributed, but where the necessity of correctness proofs was so
strong (control of nuclear power plants) that synchronous languages were
used.  In these languages, there is no distribution of control, but
distribution of data and all computations are finished when a new flow of
data arrives.   Although the system for power plant control leads naturally
to the use of a distributed model, the need for specifications of the
properties, and the proof of the satisfaction of these properties,
overrides the other aspects.

Our statement can now be summarized in this way:
in order to have  a complete cycle for the development of software dealing
with distributed systems,  there must be a way of specifying needs and
expected properties, specific to distributed systems, that is distinct from
the programming model that is used.

In this statement we do not mean that specification and programming should
be completely different. There should be pathways from one to the other,
but there should be a clear distinction between them.
 We can take the formal method B as an example.  It covers  within the same
formalism both the specification stage and the programming stage, and there
are operations restricted to each stage, which ensures that specifications
of needs are not expressed the same way as the programs that fill these
needs.
Formal models like Petri Nets have taken a different approach, and one of
their aims is to bring together specification and programming, but this
could be a hindrance for users, who see specifications as too complex, and
undistinguishable from programs.

Several formalisms can be envisaged, but there is still considerable work
to be done.  One of the main formalisms is temporal logic, which can
typically express properties of safety and liveness.  There are many
studies concerning properties related to dynamicity -  dynamicity of
modules and dynamicity of links.   Most of them deal with the programming
models and their related semantics.  This effort should be complemented
with research on  ways of specifying what is expected from dynamic systems,
such as the fact that one module can be replaced by another,  or that two
modules have to be on different processors.

This type of research will help to fill in an existing gap in the
development of programs for distributed systems.