Tipo de documento:	Relatório de Pesquisa
Título:	Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
Autor(a):	Romario Lira Batista
Orientador(a):	Christophe Saint-Christie de Lima Xavier
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.
Palavras-chave:	Redes de Petri Compiladores Prototipação
Área de conhecimento - CNPQ:	CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
Idioma:	pt_BR
País de publicação:	Brasil
Editor:	Universidade Federal do Amazonas
Sigla da Instituição:	UFAM
Faculdade, Instituto ou Departamento:	Instituto de Ciências Exatas e Tecnologia - Itacoatiara
Nome do programa:	PROGRAMA PIBIC 2011
Tipo de acesso:	Acesso Aberto
URI:	http://riu.ufam.edu.br/handle/prefix/2618
Data do documento:	31-jul-2012
Aparece nas coleções:	Relatórios finais de Iniciação Científica - Ciências Exatas e da Terra

Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.