Verification of Distributed Programs
DOI:
https://doi.org/10.59471/raia202387Keywords:
distributed program, verification, axiomaticsAbstract
This article completes our series of four articles on the axiomatic verification of programas, which we propose within the framework of the CAETI project to build an environment to support software development. In particular, we conclude the analysis of concurrent programs begun in the previous publication, now considering the family of distributed programs, characterized by having processes with disjoint variables and that communicate through messages. As always, we highlight the principle of using axiomatics as guides for obtaining correct programs by construction, and the observation that the fundamental notions of invariant predicate and variant function constitute the methodological basis in all programming paradigms.
Metrics
References
» [AFdR80] Apt, K., Francez, N. y de Roever, W. A proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst., 2, 3, 359-385, 1980.
» [CM88] Chandy, K. y Misra J. Parallel program design: a foundation. Addison-Wesley, 1988.
» [Hoa78] Hoare, C. Communicating secuential processes. Comm. ACM, 21, 8, 666-677, 1978.
» [Jon81] Jones, C. Development methods for computer programs including a notion of interference. Technical Monograph PRG-25, Oxford University, 1981.
» [OG76a] Owicki, S. y Gries, D. An axiomatic proof technique for parallel programs. Acta Informatica, 6, 319-340, 1976.
» [OG76b] Owicki, S. y Gries, D. Verifying properties of parallel programs: an axiomatic approach.
Comm. ACM, 19, 5, 279-285, 1976.
» [Ros22a] Rosenfeld, R. Introducción a la verificación de programas. Revista Abierta de Informática Aplicada, 6, 1, 79-100, 2022.
» [Ros22b] Rosenfeld, R. Verificación de programas no determinísticos. Revista Abierta de Informática Aplicada, 6, 2, 54-79, 2022.
» [Ros23] Rosenfeld, R. Verificación de programas paralelos. Revista Abierta de Informática Aplicada, 7, 1, 67-93, 2023.
» [SS84]Schlichting, R. y Schneider, F. Message passing for distributed programming. ACM Trans. Prog. Lang. Syst., 6, 3, 402-431, 1984.
» [XdRH97] Xu, Q., de Roever, W y He, J. The rely-guarantee method for verifying shared variable concurrent pograms. Formal Aspects of Computing, 9, 2, 149-174, 1997.
Published
How to Cite
Issue
Section
License
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
The article is distributed under the Creative Commons Atribución-NoComercial 4.0. Unless otherwise stated, associated published material is distributed under the same licence.
