[en] FOMAL ANALYSIS OF PROTOCOLS AND DISTRIBUTED ALGORITHMS: A BASED-LANGUAGE APPROACH

• Main Author: CARLOS BAZILIO MARTINS
• Other Authors: EDWARD HERMANN HAEUSLER
• Language: pt
• Published: MAXWELL 2006
• Subjects: [pt] PROTOCOLO; [en] PROTOCOL; [pt] ALGORITIMOS DISTRIBUIDOS; [en] DISTRIBUTED ALGORITHMS; [pt] VERIFICACAO FORMAL; [en] FORMAL VERIFICATION; [pt] ESPECIFICACAO FORMAL; [en] FORMAL SPECIFICATION
• Online Access: https://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=8074@1; https://www.maxwell.vrac.puc-rio.br/Busca_etds.php?strSecao=resultado&nrSeq=8074@2; http://doi.org/10.17771/PUCRio.acad.8074

[pt] Neste trabalho propomos uma arquitetura para a verificação formal de protocolos e algoritmos distribuídos. Esta pode ser vista como uma camada mais abstrata sobre o processo tradicional de verificação formal, onde temos a especificação e propriedade a serem verificadas, o verificador e o resultado retornado por este. O objetivo é simplificar o processo de especificação e verificação formal de protocolos e algoritmos distribuídos através de um ambiente mais dedicado. A parte principal desta arquitetura é a linguagem de especificação LEP, que contém construções de domínio-especifíco para simplificar a especificação destes sistemas. Outra característica desta linguagem é separar as especificações da topologia e do protocolo propriamente dito. Acreditamos que esta separação é válida pois torna mais clara a intenção das partes e ainda permite, por exemplo, o reuso de uma topologia entre diferentes especificações de protocolos. Assim, visamos oferecer uma linguagem cujos exemplos de especificações devem se assemelhar às descrições de algoritmos encontradas nos livros didáticos. Além disso, de forma a se ter a entrada e a saída dos verificadores formais de forma a obter a saída no nível de abstração de LEP. === [en] In this work we propose an architecture for the formal verification of protocols and distribued algoritms. This can be see as a more abstract layer over the ordinary process of formal verification, where we have just the specification of the protocol and properties to be verified, and the formal tool. Our goal is to simplifu the specification and formal verification of protocols and distributed algorithms through a dedicated environment. The core of the architecture is its input specification language (Lep), which provides domain-specific constructions for simplifying the specification of those systems. With LEP the specification of the protocol and the specification of the topology to be referred to protocol are given separetely. We feel that this division improves the legibility of both and allows the reuse of the specification of a topology among distinct protocols. Using this approach we try to offer a language whose specifications should be similar to the descriptions of the algorithms found on the didactic books. Moreover, in order to have the input and output of the architecture compatible, we also propose a way of processing the result of the formal verification tool. Then we could have the result on the abstract level of LEP.