Communication Extended Abstract Types in the refinement of parallel communicating processes

A systematic refinement transformation of a program involving processes communicating through simple rendez-vous type connections is described. Both new connections and new processes are introduced in the refined program form. The refinement is based in the concept of Communications Extended Abstract Type (CAT), which is also covered, and it amounts to either selecting, or unhiding, a CAT implementation.This refinement approach is made possible in the framework of a notation, PADD, which treats parallelism and parametric abstract types as two independent entities, combining them simply. Then, the operations of CAT implementations may involve parallel internal composition. As a consequence, a CAT may have both behavioral (unrefined) as well as structural (refined) implementations.A framework for the organization and partition of correctness proofs, including timing aspects, is given. It is based on the refinement method and the CAT concept. The constructs and tools associated with the method are being incorporated into The Llull System (TLS), the current environment for the PADD notation, being used both at the university and industry.