Export this record: EndNote BibTex

Please use this identifier to cite or link to this item: http://tede2.pucrs.br/tede2/handle/tede/5197
Document type: Dissertação
Title: Uma biblioteca de padrões de especificação em Event-B para mecanismos de troca de mensagens em sistema distribuídos
Author: Pivetta, Paulo Junior Penna 
Advisor: Dotti, Fernando Luís
Abstract (native): O desenvolvimento de sistemas distribuídos e protocolos de comunicação é uma tarefa complexa e o uso de técnicas de especificação e verificação formal torna-se necessário para garantir a corretude de tais sistemas. Enquanto técnicas de model-checking passam pelo problema da explosão do espaço de estados, o uso de provadores de teoremas representa um importante recurso para verificação de sistemas com ilimitado número estados. O método formal Event-B, de uso crescente na indústria e academia, se apóia na técnica de prova de teoremas e suporta refinamento. A contribuição deste trabalho está em proporcionar uma biblioteca reusável de padrões de especificação, em Event-B, de mecanismos de troca de mensagens em sistemas distribuídos. Um padrão de especificação define a semântica de comunicação desejada em um canal, demostrando formalmente suas propriedades. Durante o desenvolvimento de um sistema distribuído, o desenvolvedor pode fazer uso destes padrões através de passos guiados de refinamento do sistema. O sistema resultante garante a semantica de comunicação definida no padrão utilizado e livra o desenvolvedor de se preocupar em definir o sistema de comunicação a partir do início e provar suas propriedades.
Abstract (english): The development of distributed systems and communication protocols is not a trivial task and the use of formal specification and verification techniques becomes necessary to assure the correctness of such systems. While model-checking techniques face the state space explosion problem, the use of theorem provers is an important resource for verification of systems with unlimited number of states. The formal method Event-B, increasingly being used in both industry and academia, is based on the technique of theorem proving and also supports refinement. The contribution of this work is a library of reusable formal specification patterns, in Event-B, for message passing mechanisms commonly employed in distributed systems. A specification pattern defines the desired communication semantics of a channel, having its properties formally proven. During the development of a distributed system, the developer may use these patterns by applying guided refinement steps on the target model. The resulting system is assured to have the communication semantics as defined by the pattern, thus freeing the developer of defining the communication system from scratch and of proving its properties.
Keywords: INFORMÁTICA
SISTEMAS DISTRIBUÍDOS
PROTOCOLOS DE COMUNICAÇÃO
CNPQ Knowledge Areas: CNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO
Language: por
Country: BR
Publisher: Pontifícia Universidade Católica do Rio Grande do Sul
Institution Acronym: PUCRS
Department: Faculdade de Informáca
Program: Programa de Pós-Graduação em Ciência da Computação
Citation: PIVETTA, Paulo Junior Penna. Uma biblioteca de padrões de especificação em Event-B para mecanismos de troca de mensagens em sistema distribuídos. 2010. 112 f. Dissertação (Mestrado em Ciência da Computação) - Pontifícia Universidade Católica do Rio Grande do Sul, Porto Alegre, 2010.
Access type: Acesso Aberto
URI: http://tede2.pucrs.br/tede2/handle/tede/5197
Issue Date: 19-Mar-2010
Appears in Collections:Programa de Pós-Graduação em Ciência da Computação

Files in This Item:
File Description SizeFormat 
444044.pdfTexto Completo1.48 MBAdobe PDFThumbnail

Download/Open Preview


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.