Streamlining progress-based derivations of concurrent programs |
| |
| Authors: | Brijesh Dongol Arjan J Mooij |
| |
| Affiliation: | (1) ARC Centre for Complex Systems, School of Information Technology and Electrical Engineering, The University of Queensland, Brisbane, Australia;(2) School of Computer Science and Information Technology, The University of Nottingham, Nottingham, UK |
| |
| Abstract: | The logic of Owicki and Gries is a well-known logic for verifying safety properties of concurrent programs. Using this logic,
Feijen and van Gasteren describe a method for deriving concurrent programs based on safety. In this work, we explore derivation
techniques of concurrent programs using progress-based reasoning. We use a framework that combines the safety logic of Owicki
and Gries, and the progress logic of UNITY. Our contributions improve the applicability of our earlier techniques by reducing
the calculational overhead in the formal proofs and derivations. To demonstrate the effectiveness of our techniques, a derivation
of Dekker’s mutual exclusion algorithm is presented. This derivation leads to the discovery of some new and simpler variants
of this famous algorithm.
Author Mooij performed this research at the Department of Mathematics and Computer Science of the Technische Universiteit
Eindhoven, while being supported by the NWO under project 016.023.015: “Improving the Quality of Protocol Standards”.
E. C. R. Hehner |
| |
| Keywords: | Concurrent programs Mathematical techniques Program derivation Progress |
| 本文献已被 SpringerLink 等数据库收录！ |
|
