Verificación de Programas Distribuidos
DOI:
https://doi.org/10.59471/raia202387Palabras clave:
programa distribuido, verificación, axiomáticaResumen
Este artículo completa nuestra serie de cuatro artículos sobre la verificación axiomática de programas, que planteamos en el marco del proyecto del CAETI para construir un ambiente de soporte al desarrollo de software. En particular, concluimos el análisis de los programas concurrentes iniciado en la publicación anterior, considerando ahora la familia de los programas distribuidos, caracterizados por contar con procesos con variables disjuntas y que se comunican mediante mensajes. Como siempre, destacamos el principio de utilizar las axiomáticas como guías para la obtención de programas correctos por construcción, y la observación de que las nociones fundamentales de predicado invariante y función variante constituyen la base metodológica en todos los paradigmas de programación.
Métricas
Citas
» [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.
Publicado
Cómo citar
Número
Sección
Licencia
Esta obra está bajo una licencia internacional Creative Commons Atribución-NoComercial 4.0.
Este artículo se distribuye bajo la licencia Creative Commons Atribución-NoComercial 4.0. A menos que se indique lo contrario, el material publicado asociado se distribuye bajo la misma licencia.
