Algebraic specification of concurrent systems (Q914405): Difference between revisions

There exists in semantics a well developed theory of algebraic specifications of data types. The theory of process algebras for expressing the meaning of concurrent processes is widely investigated. In this paper, which is based on the author's Thèse d'Etat at the Université de Paris-Sud from 1987 (based on research performed at the Weizmann institute) the two semantic frameworks above are fused together in a single theory based on algebraic specifications. The data part of a semantic theory is described by a standard algebraic specification - its meaning is the set of all models from extended theories which satisfy the additional property of hierarchical consistency, meaning that the essential meaning of the core algebra is preserved under the extension of the signature by new data types and operators. The process part is specified using some standard form of process algebra, where the author has chosen for a trace based semantics. The two parts of the semantic framework are coupled together by means of an application operator which expresses how a process transforms its data. Processes with the same effect on all data form classes in the observational congruence. The central part of the paper deals with process refinement, investigated from the specification vs. implementation perspective. The key difficulty with process refinement relates the parallel operator from process algebra; in order that a refinement step is correct within a concurrent system the author introduces a serializability condition which tells that, with respect to the observational part of the semantics the substeps refining an atomic action in the specification can be grouped together without changing the result of applying the actions on the data. Given this condition for atomic actions the correctness of the implementation can be concluded by direct algebraic means. The paper ends with extensions and themes for further research.