Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
Carregando...
Data
Orientador(es)
Coorientador(es)
Membros da banca
Caldas, Ruiter Braga
Cavalcante, Cícero Augusto Mota
Cavalcante, Cícero Augusto Mota
Pós-Graduação
Título da Revista
ISSN da Revista
Título de Volume
Editor
Universidade Federal do Amazonas
Tipo
Direito de acesso
DOI
Resumo
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.
Abstract
This work describes a methodology for automatic code generation for embedded systems, from a Petri net, in order to minimize the time spent in coding the program and fully automate the process of transformation. The proposed approach adopts the executable specification based on Petri Nets, where can be verified some of their properties such as deadlock, liveness, boundedness, reachability among others. Petri nets contain transitions that may have annotated codes in the C and NXC programming language, that perform specific parts of the system that is being modeled. Additionally, the annotated codes in the C programming language will be verified by a Bounded Model Checker, that it will test specific properties in the code, as a index of arrays, division by zero, safety pointers and other. This specification provides the basis for the user to display the functionality of the system that will be modeled, giving the user an overview of the specific features of the system. Thus, this methodology contributes to developers and software engineers in the generation of prototypes that represent an executable specification, facilitating the evaluation of different models and helping to reduce differences of interpretation in the construction of software. This work also presents a tool called PNTCG (Petri Net Tool for Code Generation) developed based on this methodology and a case study based on a prototype automation product packaging, which uses a conveyor belt and a robot arm to demonstrate the use and application of this methodology.
Descrição
Palavras-chave
Termo controlado
Sistema embutido; Linguagem de programação C; Linguagem de programação NXC; Deadlock; Geração de protótipos
Objetivos de Desenvolvimento Sustentável (ODS)
Citação
XAVIER, Christophe Saint-Christie de Lima. Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados. 2011. 72 f. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas, Manaus, 2011.
Coleções
Avaliação
Revisão
Suplementado Por
Referenciado Por
Licença Creative Commons
Exceto quando indicado de outra forma, a licença deste item é descrita como Acesso Aberto