A formal approach for the specification of communications in distributed systems

We address the formal specification and the validation of the communication mechanisms used to implement explicit message passing in applications on MIMD systems. More precisely, we focus on the MPI standardized model which, to our knowledge, has never been given a formal specification. However, in our opinion, to be useful in practice such a standard must be accompanied by a document that gives it a formal semantics. Hence, we propose a model for the formal description of MPI, together with a specification of the overall communication architecture and of the main MPI primitives in this model. The correctness of the resulting LOTOS descriptions has been verified by simulation and by formal verification for some of them.