BDBComp
Parceria:
SBC
Derivação formal de estruturas distribuídas

Osvaldo Sérgio Farhat de CarvalhoVladimir O. Di Iorio

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 é frequentemente 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.

http://www.lbd.dcc.ufmg.br/colecoes/sbac-pad/1994/003.pdf

Caso o link acima esteja inválido, faça uma busca pelo texto completo na Web: Buscar na Web

Biblioteca Digital Brasileira de Computação - Contato: bdbcomp@lbd.dcc.ufmg.br
     Mantida por:
LBD