Formal specification of Manifold: a preliminary study
E.P.B.M. Rutten, Farhad Arbab, Iván Herman · Data Archiving and Networked Services (DANS) · 1992
This report is an initial version of a formal specication of the Manifold language.A detailed informal specication of Manifold already exists and has been used as the basis of its rst implementation.The work on formal specication of Manifold overlapped this implementation eort and they both aected the details of the informal specication of the language.In this report, we present an operational semantics of the event-driven mechanism of the Manifold language.Manifold is a parallel programming language where processes called manifolds use an event-driven control mechanism to coordinate the communications among other processes (manifolds as well as external).Inter-process communication in Manifold is through broadcast of events and a dynamic data-ow n e t work, built out of streams carrying units of data.In this report we consider only the event mechanism of Manifold, which handles the control aspect of the language.The aspect of the language concerning the exchange of data, i.e., its streams and units, is not covered in this paper.The behavior of Manifold is formally dened using transition systems at dierent structural levels.These transition systems dene the control behavior of the Manifold language constructs, from primitive actions to entire applications involving multitudes of concurrent processes.This formal specication is intended as a preliminary study.Analysis of the properties of this model has not yet been carried out.The present formal specication constitutes a basis for further work on abstract models of Manifold.C o n tinuation of this work includes clarication of the complete behavior of Manifold, development of programming assistance tools for analysis of Manifold programs, further development o f t h e Manifold model, and possibly better models for its future implementations.