A Process Specification Formalism¹

Article type: Research Article

Authors: Mauw, S. | Veltink, G.J.

Affiliations: Programming Research Group, University of Amsterdam, P.O. Box 41882, 1009 DB Amsterdam, Netherlands

Note: [1] This work was partially supported by ESPRIT contract no. 432, An integrated formal approach to industrial software development (METEOR).

Abstract: Traditional methods for programming sequential machines are inadequate for specifying parallel systems. Because debugging of parallel programs is hard, due to e.g. non-deterministic execution, verification of program correctness becomes an even more important issue. The Algebra of Communicating Processes (ACP) is a formal theory which emphasizes verification and can be applied to a large domain of problems ranging from electronic circuits to CAM architectures. The manual verification of specifications of small size has already been achieved, but this cannot easily be extended to the verification of larger industrially relevant systems. To deal with this problem we need computer tools to help with the specification, simulation, verification and implementation. The first requirement for building such a set of tools is a specification language. In this paper we introduce PSFd (Process Specification Formalism – draft) which can be used to formally express processes in ACP. In order to meet the modern requirements of software engineering, like reusability of software, PSFd supports the modular construction of specifications and parameterization of modules. To be able to deal with the notion of data, ASF (Algebraic Specification Formalism) is embedded in our formalism. As semantics for PSFd a combination of initial algebra semantics and operational semantics for concurrent processes is used. A comparison with programming languages and other formal description techniques for the specification of concurrent systems is included.

DOI: 10.3233/FI-1990-13202

Journal: Fundamenta Informaticae, vol. 13, no. 2, pp. 85-139, 1990