Abstract
Currently software engineering practices use relatively few formal methods. However, formal methods can be used to find errors earlier in the software cycle and hence reduce software cost. One useful formal method is program verification. The axiomatic approach to program verification uses assertions to characterize properties of program variables and relationships between them at various stages of program execution. In order to verify these assertions, axioms or inference rules are needed for each statement as well as some statement-independent inference rules. The message passing and nondeterminism of a distributed programming language present special difficulties. This paper examines and compares three approaches to handling the message passing and nondeterminism of CSP, which is Hoare's model language for distributed programming, as well as the basic concepts of program verification for sequential processing. The paper culminates in a series of transformations which show the equivalence of the three approaches.
Recommended Citation
Lutfiyya, Hanan and McMillin, Bruce M., "Comparison of Three Axiomatic Systems for CSP" (1991). Computer Science Technical Reports. 127.
https://scholarsmine.mst.edu/comsci_techreports/127
Department(s)
Computer Science
Report Number
CSc-91-07
Document Type
Technical Report
Document Version
Final Version
File Type
text
Language(s)
English
Rights
© 1991 University of Missouri - Rolla, All rights reserved
Publication Date
1991-06-06
Comments
The first Author is a Graduate Student.
This work was supported in part by the National Science Foundation under Grant Numbers MIP-8909749 and CDA-8820714, and in part by the AMOCO Faculty Development Program.