Formal prototyping of concurrent systems
Bart J. Geraci · 1993
Prototyping has been proposed as an alternative to the traditional waterfall approach for designing software systems. The corresponding methodology consists of an ad-hoc mixture of language, tools, and methods. Although there are a few systems available for prototyping concurrent programs, they lack some important features. One problem is that some of these systems are limited to paper designs; there is no implementation available. A larger problem is that these systems lack a formal basis for their language and translation method definitions. A programming system, Ripple, is proposed for prototyping parallel and distributed programs. The proposed environment to support the prototyping methodology consists of a hierarchy of three languages (TPL, SPL, IPL), a set of tools, and a hierarchical method. TPL is a process language designed to express the structure of the prototype without describing the details of functions. SPL is a specification language designed to describe the functions in an abstract specification. IPL is a programming language that can be implemented on a given system. It will be shown how TPL can be formally converted into SPL and in turn be translated into IPL. The Ripple languages have been designed with the two important features found lacking in previous systems. The formality of the Ripple languages and the translation from one language to the other implies that the meanings of TPL programs are preserved throughout the hierarchy. In addition, this formal basis provides a framework for various static analysis tasks. Finally, a compiler was built to show the feasibility of translating a kernel of TPL to both SPL and IPL.