Derivação Formal de Estruturas Distribuídas
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 expressada através de um predicado que deve ser mantido invariante. Por exemplo, uma estrutura associada com o problema da exclusão mútua possui componentes que descrevem o estado atual de cada sítio - usando ou não o recurso compartilhado - e o predicado que expressa correção exige que dois ou mais sítios não podem estar utilizando o recurso simultaneamente. 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 2 nós, mostramos que qualquer predicado é equivalente a uma desigualdade sobre um domínio parcialmente ordenado adequadamente escolhido.
Referências
Daniel Barbara e Hector Garcia-Molina. Mutual exclusion in partitioned distributed systems. Distributed Computing, 1:119-132, 1986.
Osvaldo S. F. Carvalho e Gerard Roucairol. On mutual exclusion in computer networks. Communications of the ACM, 26(2), February 1983.
K. M. Chandy e J. Misra. The Drinking Philosophers Problem. ACM Transactios on Programming Languages and Systems, 6(4):632-646, October 1984.
Edward G. Coffman e Peter J. Denning. Operating Systems Theory. Prentice-Hall, 1973.
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.
Per Brinch Hansen. Operating System Principies. Prentice-Hall, 1973.
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.
Oysten Ore. "Galois Connections". Transactions of the American Mathematical Society, 55:493513, 1944.
S. Owick e D. Gries. Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19(5), May 1976.
G. Ricart e A. K. Agrawala. "An Optimal Algorithm for Mutual Exclusion in Compu ter Networks". Communications of the ACM, 24(1), January 1981.
Richard L. Schwartz e P. Michael Melliar-Smith. "From State Machines to Temporal Logic: Specification Methods for Protocol Standars". IEEE Transactions on Communications, 30(12):2486-2496, December 1982.
Alan C. Shaw. The Logical Design of Operating Systems. Prentice-Hall, 1974.
G. Szasz. Introduction to Lattice Theory. Academic Press, 1963.
Andrew S. Tanenbaum. Modem Operating Systems. Prentice Hall, 1992.
