Proposta de uma abordagem para a verificação formal de Sistemas Distribuídos Baseados em Objetos - Santos, Osmar Marchi dos; Dotti, Fernando Luís (Anais do Workshop de Testes e Tolerância a Falhas (WTF), 2003)
Este artigo propõe uma abordagem para a verificação formal, através da técnica de verificação de modelos, de Sistemas Distribuídos Baseados em Objetos (SDBOs). A linguagem de descrição utilizada para modelar SDBOs é uma forma restrita de Gramática de Grafos, um formalismo gráfico, declarativo, e que suporta paralelismo implícito. Esta linguagem, chamada Gramática de Grafos Baseada em Objetos (GGBO), é brevemente apresentada. Os modelos descritos na GGBO são mapeados para a linguagem de descrição PROMELA (PROtocol/PROcess MEta LAnguage), usada pelo verificador de modelos SPIN (Simple Promela INterpreter). Este mapeamento é descrito. A partir disso, propriedades sobre modelos descritos na GGBO podem ser especificadas e verificadas através do SPIN. Um exemplo de descrição na GGBO é apresentado e mapeado.