[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.
| Identifer | oai:union.ndltd.org:puc-rio.br/oai:MAXWELL.puc-rio.br:8074 |
| Date | 03 April 2006 |
| Creators | CARLOS BAZILIO MARTINS |
| Contributors | EDWARD HERMANN HAEUSLER |
| Publisher | MAXWELL |
| Source Sets | PUC Rio |
| Language | Portuguese |
| Detected Language | English |
| Type | TEXTO |
Page generated in 0.002 seconds