How to invent distributed implementation schemes of an object-based concurrent language: a transformational approach

摘要

A design and verification technique for implementation schemes of distributed software is presented. In this technique, first, the specification is modelled by a concurrent object system, that is, one which is constituted of computational agents with capability of concurrent execution and message passing. Then, such a concurrent object system is transformed into another concurrent object system, which models a sophisticated implementation scheme.

rn

Our transformation technique is mainly based on fusing and splitting concurrent objects. The correctness of transformation rules can be proven formally.