Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados

• Ano de defesa: 2011
• Autor(a) principal: Xavier, Christophe Saint-Christie de Lima
• Outros Autores: http://lattes.cnpq.br/3228997034387953
• Tipo de documento: Dissertação
• Tipo de acesso: Acesso aberto
• Idioma: por
• Instituição de defesa: Universidade Federal do Amazonas; Instituto de Computação; Brasil; UFAM; Programa de Pós-graduação em Informática
• Palavras-chave em Português: Sistema embutido; Linguagem de programação C; Linguagem de programação NXC; Geração de protótipos; Deadlock; CIÊNCIAS EXATAS E DA TERRA; Redes de Petri; Compiladores; Prototipação; Bounded Model Checker
• Link de acesso: https://tede.ufam.edu.br/handle/tede/8490

Este trabalho descreve uma metodologia para a geração automática de código para sistemas embarcados, a partir de uma rede de Petri, com objetivo de minimizar o tempo gasto na codificação do programa e automatizar completamente o processo de transformação. A abordagem proposta utiliza uma Especificação Executável baseada em Redes de Petri, onde nesta pode ser verificado algumas de suas propriedades como deadlock, vivacidade, limitação, alcançabilidade, dentre outras. As Redes de Petri contêm transições que podem ter códigos anotados na linguagem de programação C e NXC, que executarão partes específicas do sistema que estará sendo modelado. Adicionalmente, os códigos anotados na linguagem de programação C serão verificados por um Bounded Model Checker, que testará propriedades específicas do código, como limite de arrays, divisão por zero, segurança de ponteiros e outras. Esta especificação serve de base para exibir ao usuário as funcionalidades do sistema que será modelado, proporcionando ao usuário uma visão das características específicas do sistema. Desta forma, contribuindo com desenvolvedores e engenheiros de software na geração de protótipos que constituem uma especificação executável, facilitando a avaliação de diferentes modelos e ajudando a reduzir as diferenças de interpretação na construção de software. Este trabalho também apresenta uma ferramenta denominada de PNTCG (Petri Net Tool for Code Generation) desenvolvida com base nesta metodologia e um estudo de caso baseado em um protótipo de automatização de embalagens de produto, no qual, é utilizado uma esteira e um braço robô para demonstrar a utilização e aplicação da metodologia proposta.