Título: | FOMAL ANALYSIS OF PROTOCOLS AND DISTRIBUTED ALGORITHMS: A BASED-LANGUAGE APPROACH | |||||||
Autor: |
CARLOS BAZILIO MARTINS |
|||||||
Colaborador(es): |
EDWARD HERMANN HAEUSLER - Orientador |
|||||||
Catalogação: | 03/ABR/2006 | Língua(s): | PORTUGUESE - BRAZIL |
|||||
Tipo: | TEXT | Subtipo: | THESIS | |||||
Notas: |
[pt] Todos os dados constantes dos documentos são de inteira responsabilidade de seus autores. Os dados utilizados nas descrições dos documentos estão em conformidade com os sistemas da administração da PUC-Rio. [en] All data contained in the documents are the sole responsibility of the authors. The data used in the descriptions of the documents are in conformity with the systems of the administration of PUC-Rio. |
|||||||
Referência(s): |
[pt] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=8074&idi=1 [en] https://www.maxwell.vrac.puc-rio.br/projetosEspeciais/ETDs/consultas/conteudo.php?strSecao=resultado&nrSeq=8074&idi=2 |
|||||||
DOI: | https://doi.org/10.17771/PUCRio.acad.8074 | |||||||
Resumo: | ||||||||
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.
|
||||||||