Derivação Formal de Estruturas Distribuídas - Carvalho, Osvaldo S. F.; Di Iorio, Vladimir O. (Anais do International Symposium on Computer Architecture and High Performance Computing (SBAC-PAD), 1994)
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.