Structured Specification of Communicating Systems
- 1 February 1983
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-32 (2) , 120-133
- https://doi.org/10.1109/tc.1983.1676197
Abstract
Specification methods for distributed systems is the underlying theme of this paper. A model of communicating processes with rendezvous interactions is assumed as a basis for the discussion. The possible interactions by a process, and the interconnection between several subprocesses within a process are specified using the concept of ports, which are specified separately. Step-wise refinement of process specifications and associated verification rules are considered. The step-wise refinement of port specifications and associated interactions is considered as well. After the presentation of an introductory example, the paper discusses the basic concepts of the specification method. They are then applied to more complex examples. The step-wise wefinement of ports and interactions is demonstrated by a hardware interface for which an abstract specification and a more detailed implementation is given. Proof rules for verifying the consistency of detailed and more abstract specifications are discussed in some detail.Keywords
This publication has 23 references indexed in Scilit:
- Port directed communicationThe Computer Journal, 1981
- Rationale for the design of the Ada programming languageACM SIGPLAN Notices, 1979
- Communicating sequential processesCommunications of the ACM, 1978
- Software Descriptions with Flow ExpressionsIEEE Transactions on Software Engineering, 1978
- A language for formal problem specificationCommunications of the ACM, 1977
- Abstract data types and the development of data structuresCommunications of the ACM, 1977
- A Language Extension for Controlling Access to Shared DataIEEE Transactions on Software Engineering, 1976
- An Introduction to the Construction and Verification of Alphard ProgramsIEEE Transactions on Software Engineering, 1976
- Formal verification of parallel programsCommunications of the ACM, 1976
- Guarded commands, nondeterminacy and formal derivation of programsCommunications of the ACM, 1975