Return to search

Uma abordagem para modelagem e verificação de protocolos síncronos de barramentos de comunicação

Dissertação (mestrado) - Universidade Federal de Santa Catarina, Centro Tecnológico. Programa de Pòs-graduação em Engenharia de Automação e Sistemas / Made available in DSpace on 2012-10-24T06:53:00Z (GMT). No. of bitstreams: 1
262665.pdf: 898231 bytes, checksum: 7df3af7aeaef56963e32dd13df0af1fb (MD5) / Este trabalho apresenta um estudo a respeito de protocolos para barramentos de comunicação, enfatizando os aspectos de parametrização e sincronização vistos em tais protocolos. De acordo com estas características e sua influência na modelagem e verificação de sistemas que utilizam os barramentos, buscaram-se métodos e ferramentas adaptados a sistemas embarcados, síncronos e parametrizados. A abordagem utilizada neste trabalho consiste na especificação de protocolos em duas perspectivas distintas para ressaltar tanto os aspectos da arquitetura dos sistemas com barramento quanto o comportamento descrito pelos protocolos. A modelagem de arquitetura foi realizada com a utilização da linguagem de descrição de arquitetura AADL. A modelagem de comportamento utilizou a linguagem síncrona LUSTRE para permitir a criação de um modelo de fácil compreensão e simulação. O método Event-B foi escolhido para a modelagem e verificação comportamental e sua semântica orientada a refinamentos permitiu a criação de um modelo de base abstrato e genérico que pode ser reutilizado em protocolos síncronos com arbitração centralizada. A partir deste modelo, os protocolos PCI e AMBA foram utilizados como estudo de caso para especificação e verificação.

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufsc.br:123456789/92220
Date January 2009
CreatorsFrança, Ricardo Bedin
ContributorsUniversidade Federal de Santa Catarina, Farines, Jean Marie, Becker, Leandro Buss
PublisherFlorianópolis, SC
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/masterThesis
Sourcereponame:Repositório Institucional da UFSC, instname:Universidade Federal de Santa Catarina, instacron:UFSC
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0033 seconds