metadata.dc.type:	Relatório de Pesquisa
Title:	Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
metadata.dc.creator:	Romario Lira Batista
metadata.dc.contributor.advisor1:	Christophe Saint-Christie de Lima Xavier
metadata.dc.description.resumo:	Nos diferentes ambientes de Sistemas Embarcados, aplicações de softwares necessitam ser desenvolvidas rapidamente e atender a um alto nível de qualidade. Os métodos formais desempenham um importante papel para mensurar a previsibilidade e dependência no projeto de aplicações critica. Como exemplo, podemos citar as Redes de Petri para modelagem de tais sistemas, objetivando a verificação das propriedades dos mesmos, assim como o seu devido comportamento. O uso de métodos formais no desenvolvimento de softwares apresenta varias vantagens, por exemplo, programas (ou protótipos) podem ser gerados automaticamente e formalmente a partir de suas especificações. Tais protótipos, algumas vezes chamados de especificações executáveis, servem de base para exibir a o usuário as funcionalidades do futuro sistema. Pode-se provar também que determinados programas satisfazem determinadas propriedades e que o programa é uma realização da sua especificação. A especificação executável permite evitar inconsistências, erros e garantir a completude do sistema. Esse processo assegura uma interpretação não ambígua para a especificação do sistema, valida a funcionalidade do sistema antes do inicio da sua implementação e cria modelos de desempenho do sistema e avalia o desempenho do sistema. Segundo [Budde et al., 1992], protótipos adequados fornecem aos usuários e gestores uma idéia tangível das soluções dos problemas. Para os desenvolvedores, os protótipos que constituem uma especificação executável que facilita a avaliação de diferentes modelos e ajuda a reduzir as diferenças de interpretação na construção de softwares [Alcoforado, 2007]. Este trabalho propõe gerar uma especificação executável baseada em um modelo formal conhecido como Redes de Petri focado para Redes de Petri Colorida, no qual é possível checar propriedades especificas e características de uma Rede de Petri, tais como, se a rede é segura, limitada, ordinária, pura, possuem deadlock, entre outras. Nesta, contem transições e lugares que possuem códigos anotados na linguagem C ou NXC, onde adicionalmente o código C passará por uma verificação formal usando um Bounded Model Checker para comprovar o comportamento e assegurar as propriedades definidas no código e, com base nestes itens, é efetuada a geração do código. Este trabalho também apresentará a ferramenta denominada de PNTCG (Petri Net Tool for Code Generation) a ser otimizada utilizando Redes de Petri Colorida com base nesta metodologia e um estudo de caso baseado em um protótipo de automatização de embalagens de produtos, no qual é utilizado uma esteira e um braço robô para demonstrar a utilização e aplicação da metodologia proposta.
Keywords:	Redes de Petri Compiladores Prototipação
metadata.dc.subject.cnpq:	CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
metadata.dc.language:	pt_BR
metadata.dc.publisher.country:	Brasil
Publisher:	Universidade Federal do Amazonas
metadata.dc.publisher.initials:	UFAM
metadata.dc.publisher.department:	Instituto de Ciências Exatas e Tecnologia - Itacoatiara
metadata.dc.publisher.program:	PROGRAMA PIBIC 2011
metadata.dc.rights:	Acesso Aberto
URI:	http://riu.ufam.edu.br/handle/prefix/2618
Issue Date:	31-Jul-2012
Appears in Collections:	Relatórios finais de Iniciação Científica - Ciências Exatas e da Terra

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.