Specification and verification of a network mail system
Techniques for describing and verifying modular systems are illustrated using a simple network mail problem. The design is presented in a top-down style. At each level of refinement, the specifications of the higher level are verified from the specifications of lower level components.
KeywordsLocal User Error Message Message Delivery Exit Condition Proof Outline
Unable to display preview. Download preview PDF.
- Owicki, S., Specifications and Proofs for Abstract Data Types in Concurrent Programs, in this volume.Google Scholar
- Brinch Hansen, P., Network, a Multiprocessor Program. IEEE Trans on Software Engineering, v. 4, no. 3 (May, 1978) 194–199.Google Scholar
- Ambler, A., et al., A Language for Specification and Implementation of Verifiable Programs. Proc. of an ACM Conference on Language Design for Reliable Software, SIGPLAN Notices v. 12, n.3 (also Operating Systems Review v. 11, n.2, and Software Engineering Notes, v.2, n.2) (1977) 1–10.Google Scholar
- Andrews, G., Modula and the Design of a Message Switching Communications System. TR78-329, Cornell University, Computer Science Dept. (1978)Google Scholar
- Owicki, S., Verifying Parallel Programs with Resource Allocation. Proc. International Conference on Math. Studies of Information Processing, Kyoto, Japan (1978).Google Scholar