Uma biblioteca de padrões de especificação em Event-B para mecanismos de troca de mensagens em sistema distribuídos
AUTOR(ES)
Paulo Junior Penna Pivetta
FONTE
IBICT - Instituto Brasileiro de Informação em Ciência e Tecnologia
DATA DE PUBLICAÇÃO
19/03/2010
RESUMO
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.
ASSUNTO(S)
informÁtica sistemas distribuÍdos protocolos de comunicaÇÃo ciencia da computacao
ACESSO AO ARTIGO
http://tede.pucrs.br/tde_busca/arquivo.php?codArquivo=4442Documentos Relacionados
- Uma Biblioteca para programação paralela por troca de mensagens de clusters baseados na tecnologia SCI
- Algoritmos distribuidos para localização de falhas e difusão de mensagens em hipercubos defeituosos
- Aspectos de especificação e implementação da estruta de mensagens de um sistema didatico do protocolo MMS
- Uma abordagem na camada de middleware para troca dinâmica de componentes em sistemas multimídia distribuídos baseados no framework Cosmos
- Mecanismos de controle e comunicação para sistemas especialistas distribuidos