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.