Uma Metodologia para a Verificação de Sistemas Parciais Modelados na Gramática de Grafos Baseada em Objetos - Dotti, Fernando L.; Pasini, Fábio; Santos, Osmar M. dos (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 2004: Anais do XVIII Simpósio Brasileiro de Engenharia de Software, 2004)
O desenvolvimento de sistemas distribuídos é considerado uma tarefa complexa. Em especial, garantir que estes sistemas apresentam certas propriedades, fundamentais para o seu correto funcionamento, torna-se muito difícil em ambientes abertos, como, por exemplo, a Internet. Neste artigo utilizamos uma linguagem visual de especificação formal, chamada Gramática de Grafos Baseadas em Objetos (GGBO), para a especificação e verificação de sistemas distribuídos. É proposta uma metodologia para a verificação de sistemas parciais, baseada no raciocínio assume-guarantee, definidos na GGBO. Na metodologia proposta, uma transformação é realizada sobre o objeto a ser verificado. A transformação tem como objetivo fechar (completar) o comportamento do objeto, de forma que a técnica de verificação de modelos possa ser aplicada ao mesmo. Um objeto que implementa a ordenação de mensagens é utilizado, no decorrer do artigo, para ilustrar a metodologia definida.