Título
[pt] ANÁLISE FORMAL DE PROTOCOLOS E ALGORITMOS DISTRIBUÍDOS: UMA ABORDAGEM BASEADA EM LINGUAGEM
Título
[en] FOMAL ANALYSIS OF PROTOCOLS AND DISTRIBUTED ALGORITHMS: A BASED-LANGUAGE APPROACH
Autor
[pt] CARLOS BAZILIO MARTINS
Vocabulário
[pt] PROTOCOLO
Vocabulário
[pt] ESPECIFICACAO FORMAL
Vocabulário
[pt] VERIFICACAO FORMAL
Vocabulário
[pt] ALGORITIMOS DISTRIBUIDOS
Vocabulário
[en] PROTOCOL
Vocabulário
[en] FORMAL SPECIFICATION
Vocabulário
[en] FORMAL VERIFICATION
Vocabulário
[en] DISTRIBUTED ALGORITHMS
Resumo
[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.
Resumo
[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.
Orientador(es)
EDWARD HERMANN HAEUSLER
Banca
MARKUS ENDLER
Banca
RENATO FONTOURA DE GUSMAO CERQUEIRA
Banca
CHRISTIANO DE OLIVEIRA BRAGA
Banca
EDWARD HERMANN HAEUSLER
Banca
MARIO ROBERTO F BENEVIDES
Banca
RAIMUNDO JOSE DE ARAUJO MACEDO
Catalogação
2006-04-03
Apresentação
2005-09-09
Tipo
[pt] TEXTO
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Formato
application/pdf
Idioma(s)
PORTUGUÊS
Referência [pt]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074@1
Referência [en]
https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074@2
Referência DOI
https://doi.org/10.17771/PUCRio.acad.8074
Arquivos do conteúdo
CAPA, AGRADECIMENTOS, RESUMO, ABSTRACT, SUMÁRIO E LISTAS PDF CAPÍTULO 1 PDF CAPÍTULO 2 PDF CAPÍTULO 3 PDF CAPÍTULO 4 PDF CAPÍTULO 5 PDF CAPÍTULO 6 PDF CAPÍTULO 7 PDF REFERÊNCIAS BIBLIOGRÁFICAS E APÊNDICES PDF