Especificação e Verificação Formal de Sistemas Distribuídos - Dotti, Fernando L.; Foss, Luciana; Ribeiro, Leila; Santos, Osmar M. dos (Anais do Simpósio Brasileiro de Engenharia de Software (SBES); 2003: Anais do XVII Simpósio Brasileiro de Engenharia de Software, 2003)
Neste artigo utilizamos uma linguagem visual de especificação formal, chamada Gramáticas de Grafos Baseadas em Objetos (GGBO), para especificar sistemas distribuídos. A GGBO é comparada com a linguagem PROMELA (a PROcess MEta LAnguage), usada como entrada pelo verificador de modelos SPIN. Com base nesta comparação, define-se um mapeamento de GGBO para PROMELA. É visto como especificar e verificar propriedades sobre os modelos mapeados para PROMELA. Um algoritmo de eleição em anel é utilizado, no decorrer do artigo, para ilustrar a GGBO, a tradução e a verificação de propriedades.