Please use this identifier to cite or link to this item: http://riu.ufam.edu.br/handle/prefix/2618
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.
Abstract: 
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 Restrito
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

Files in This Item:
There are no files associated with this item.


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