PSF - Process Specification Formalism

About PSF

PSF (process Specification Formalism) is a Formal Description Technique developed for the specification of concurrent systems. A description of PSF can be found in [MauVel90], [MauVel93], [Die94], and DiePon94].

PSF has been designed as the base for a set of tools to support ACP (Algebra of Communicating Processes) [BerKlo86]. It is very close to the informal syntax normally used in denoting ACP-expressions. The part of PSF that deals with the description of data is based on ASF (Algebraic Specification Formalism) [BerHeeKli89]. To meet the modern needs of software engineering, PSF supports the modular construction of specifications and the parametrization of modules.

Processes in PSF are described as a series of atomic actions combined by operators. Atomic actions are the basic and indivisible elements of processes in PSF. By using atomic actions and operators we can construct process expressions. These process expressions in combination with recursive process definitions are used to define processes. The basic operators on processes are sequential, alternative and parallel composition.

Communication between parallel processes can be defined with the communication function, which takes two atoms as arguments and returns the result of their communication. The encapsulation operator can be used to rename a set of atomic actions into delta, the constant process indicating a deadlock. This is used to enforce communication between parallel processes. The hiding operator can be used to rename a set of atomic actions into skip, the constant process indicating an internal action. This operator makes it possible to concentrate on a set of visible actions.

The language has been extended with an interrupt, disrupt, and priority mechanism ([Die94]), and also with an iteration and nesting operator ([DiePon94]).


J.A. Bergstra, J. Heering, and P. Klint, "The Algebraic Specification Formalism ASF", in Algebraic Specification, ed. J.A. Bergstra, J. Heering, P. Klint, ACM Press Frontier Series, pp 1-66, Addison-Wesley, 1989.

J.A. Bergstra and J.W. Klop, "Process Algebra: specification and verification in bisimulation semantics", in MATH. & Comp. Sci. II, ed. M. Hazewinkel, J.K. Lenstra, L.G.L.T. Meertens, eds., CWI Monograph 4, pp 61-94, North-Holland, Amsterdam, 1986.
B. Diertens, "New Features in PSF     I - Interrupts, Disrupts, and Priorities", Report P9417, Programming Research Group - University of Amsterdam, June 1994.
B. Diertens and A. Ponse, "New Features in PSF     II - Iteration and Nesting", Report P9425, Programming Research Group - University of Amsterdam, October 1994.
S. Mauw and G.J. Veltink, "A Process Specification Formalism", in Fundamenta Informaticae XIII (1990), pp. 85-139, IOS Press, 1990.
S. Mauw and G.J. Veltink (eds.), Algebraic Specification of Communication Protocols, Cambridge Tracts in Theoretical Computer Science 36, Cambridge University Press, 1993.