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

Xavier, Christophe Saint-Christie de Lima; http://lattes.cnpq.br/3228997034387953

Dissertação

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

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ç...

ver descrição completa

Autor principal:	Xavier, Christophe Saint-Christie de Lima
Outros Autores:	http://lattes.cnpq.br/3228997034387953
Grau:	Dissertação
Idioma:	por
Publicado em:	Universidade Federal do Amazonas 2021
Assuntos:	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
Acesso em linha:	https://tede.ufam.edu.br/handle/tede/8490

id	oai:https:--tede.ufam.edu.br-handle-:tede-8490
recordtype	dspace
spelling	oai:https:--tede.ufam.edu.br-handle-:tede-84902021-10-16T05:03:24Z Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados Xavier, Christophe Saint-Christie de Lima Barreto, Raimundo da Silva http://lattes.cnpq.br/3228997034387953 http://lattes.cnpq.br/1132672107627968 Caldas, Ruiter Braga http://lattes.cnpq.br/9686087091192989 Cavalcante, Cícero Augusto Mota http://lattes.cnpq.br/9293110828710584 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 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. 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. Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) 2021-10-15T22:54:32Z 2011-02-11 Dissertaçã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. https://tede.ufam.edu.br/handle/tede/8490 por Acesso Aberto http://creativecommons.org/licenses/by-nc-nd/4.0/ application/pdf Universidade Federal do Amazonas Instituto de Computação Brasil UFAM Programa de Pós-graduação em Informática
institution	TEDE - Universidade Federal do Amazonas
collection	TEDE-UFAM
language	por
topic	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
spellingShingle	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 Xavier, Christophe Saint-Christie de Lima Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
topic_facet	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
description	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.
author_additional	Barreto, Raimundo da Silva
author_additionalStr	Barreto, Raimundo da Silva
format	Dissertação
author	Xavier, Christophe Saint-Christie de Lima
author2	http://lattes.cnpq.br/3228997034387953
author2Str	http://lattes.cnpq.br/3228997034387953
title	Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
title_short	Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
title_full	Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
title_fullStr	Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
title_full_unstemmed	Especificação executável usando uma linguagem de redes de Petri no domínio de sistemas embarcados
title_sort	especificação executável usando uma linguagem de redes de petri no domínio de sistemas embarcados
publisher	Universidade Federal do Amazonas
publishDate	2021
url	https://tede.ufam.edu.br/handle/tede/8490
_version_	1831969994128228352
score	11.753896

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

Registros relacionados