XINFORMAÇÕES SOBRE DIREITOS AUTORAIS
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
As obras disponibilizadas nesta Biblioteca Digital foram publicadas sob expressa autorização dos respectivos autores, em conformidade com a Lei 9610/98.
A consulta aos textos, permitida por seus respectivos autores, é livre, bem como a impressão de trechos ou de um exemplar completo exclusivamente para uso próprio. Não são permitidas a impressão e a reprodução de obras completas com qualquer outra finalidade que não o uso próprio de quem imprime.
A reprodução de pequenos trechos, na forma de citações em trabalhos de terceiros que não o próprio autor do texto consultado,é permitida, na medida justificada para a compreeensão da citação e mediante a informação, junto à citação, do nome do autor do texto original, bem como da fonte da pesquisa.
A violação de direitos autorais é passível de sanções civis e penais.
Coleção Digital
Título: ANÁLISE FORMAL DE PROTOCOLOS E ALGORITMOS DISTRIBUÍDOS: UMA ABORDAGEM BASEADA EM LINGUAGEM Autor: CARLOS BAZILIO MARTINS
Instituição: PONTIFÍCIA UNIVERSIDADE CATÓLICA DO RIO DE JANEIRO - PUC-RIO
Colaborador(es):
EDWARD HERMANN HAEUSLER - ORIENTADOR
Nº do Conteudo: 8074
Catalogação: 03/04/2006 Liberação: 03/04/2006 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
Nota: 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.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074&idi=1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074&idi=2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.8074
Resumo:
Título: ANÁLISE FORMAL DE PROTOCOLOS E ALGORITMOS DISTRIBUÍDOS: UMA ABORDAGEM BASEADA EM LINGUAGEM Autor: CARLOS BAZILIO MARTINS
Nº do Conteudo: 8074
Catalogação: 03/04/2006 Liberação: 03/04/2006 Idioma(s): PORTUGUÊS - BRASIL
Tipo: TEXTO Subtipo: TESE
Natureza: PUBLICAÇÃO ACADÊMICA
Nota: 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.
Referência [pt]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074&idi=1
Referência [en]: https://www.maxwell.vrac.puc-rio.br/colecao.php?strSecao=resultado&nrSeq=8074&idi=2
Referência DOI: https://doi.org/10.17771/PUCRio.acad.8074
Resumo:
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.
