Derivação Formal de Algoritmos Distribuídos Utilizando Propriedades de Progresso
Resumo
Uma estrutura de dados distribuída possui n componentes, uma em cada sítio de um sistema distribuído (nós de uma rede de computadores). A correção de uma estrutura de dados distribuída é freqüentemente expressa através de um predicado que deve ser mantido invariante. Uma técnica formal para derivação de estruturas de dados distribuídas especificada por um invariante é descrita, cuja correção é definida por um predicado global. Utilizando uma rede com dois nós, mostramos que qualquer predicado é equivalente a uma desigualdade sobre um domínio parcialmente ordenado adequadamente escolhido. O modelo é aplicado a um meio de comunicação onde as mensagens podem ser perdidas ou duplicadas, mas a ordem de envio é preservada. São derivados algoritmos para solucionar problemas entre dois nós em um meio como esse, utilizando um formato mínimo para as mensagens trocadas entre os nós.
Referências
Henri E. Bal, Jennifer G. Steiner, and Andrew S. Tanenbaum. Programming Languages for Distributed Computing Systems. ACM Computing Surveys, 21(3):261-322, September 1989.
K.A. Bartlett, R.A. Scantlebury, and P.T. Wilkinson. A note on reliable full-duplex transmission over half-duplex links. Communications of the ACM, 12(5):260-261, May 1969.
Osvaldo S. F. Carvalho. One contribution à la programmation des systèmes distribués. Thèse d'État, Université Pierre et Marie Curie (Paris VI), Juillet 1985.
Osvaldo S. F. Carvalho and Vladimir O. Di Iorio. Derivação Formal de Estruturas Distribuídas. ln Anais do VI Simpósio Brasileiro de Arquitetura de Computadores e Processamento Paralelo, pages 21-35, Caxambu-MG, Junho 1994. Sociedade Brasileira de Computação.
Osvaldo S. F. Carvalho and Gerard Roucairol. On mutual exclusion in computer networks. Communications of the ACM, 26(2), February 1983.
Vladimir Oliveira Di Iorio. Derivação Formal de Estruturas Distribuídas. Dissertação de Mestrado, DCC-UFMG, Abril 1994.
E. W. Dijkstra. Guarded commands, nondeterminancy, and formal derivation of programs. Communications of the ACM, 8(18):453-457, August 1975.
Ralph P. Grimaldi. Discrete and Combinatorial Mathematics. Addison-Wesley, 1988.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 10(12):576-580, October 1969.
C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8), August 1978.
R. M. Keller. "Formal Verification of Parallel Programs". Communications of the ACM, 19(7), July 1976.
Leslie Lamport. "Time, Clocks, and the Ordering of Events in a Distributed System". Communications of the ACM, 21(7), July 1978.
Mamoru Maekawa. "A √2 Algorithm for Mutual Exclusion in Decentralized Systems". ACM Transactions on Computing Systems, 3(2), May 1985.
S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19(5), May 1976.
Oysten Ore. "Galois Connections". Transactions of the American Mathematical Society, 55:493-513, 1944.
F.B. Schneider and G.R. Andrews. Lecture notes in computer science vol. 224. In Current Trends in Concurrency, pages 669-716. Springer-Verlag, New York, 1986.
A. U. Shankar. "An Introduction to Assertional Reasoning for Concurrent Systems". ACM Computing Surveys, 25(3):225-262, September 1993.
Richard L. Schwartz and P. Michael Melliar-Smith. "From State Machines of Temporal Logic: Specification Methods for Protocol Standards". IEEE Transactions on Communications, 30(12):2486-2496, December 1982.
G. Szasz. Introduction to Lattice Theory. Academic Press, 1963.
