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 SoftwareDO - 10.5753/sbes.2003.23863, 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.