Especificação e verificação sistemática, formal e modular de sistemas embarcados.

• Ano de defesa: 2006
• Autor(a) principal: SILVA, Leandro Dias da.
• Tipo de documento: Tese
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal de Campina Grande; Brasil; Centro de Engenharia Elétrica e Informática - CEEI; PÓS-GRADUAÇÃO EM ENGENHARIA ELÉTRICA; UFCG
• Palavras-chave em Português: Redes de Petri - Desenvolvimento Baseado em Componentes.; Verificação de Sistemas Embarcados.; Desenvolvimento Baseado em Componentes.; Petri Nets - Component Based Development.; Verification of Embedded Systems.; Component Based Development.; Engenharia Elétrica.
• Link de acesso: http://dspace.sti.ufcg.edu.br:8080/jspui/handle/riufcg/3269

Este trabalho está inserido no contexto de engenharia de software baseada em componentes para o domínio de sistemas embarcados, no nível de modelagem. A fase de modelagem é importante pois permite um melhor entendimento de um dado problema e de suas possíveis soluções, além de facilitar a manutenção e a evolução do sistema. Redes de Petri Coloridas Hierárquicas (HCPN - Hierarchical Coloured Petri Nets) s˜ao utilizadas para a especificação e verificação formal de tais sistemas. A utilização de HCPN na modelagem de sistemas complexos promove a descrição de modelos de forma compacta e organizada. A utilização de componentes promove a modularização da construção do espaço de estados, utilizando descrições de suas interfaces. Para tanto, utilizamos o conceito de grafos de ocorrência com classes de equivalência para definir a interação entre os componentes do sistema, ignorando seus comportamentos internos. Além de classes de equivalência, é utilizado o formalismo Autômato com Interface Temporizado (TIA - Timed Interface Automata) para expressar as interfaces dos componentes modelados com HCPN para análise de compatibilidade.