Use este identificador para citar ou linkar para este item: http://riu.ufam.edu.br/handle/prefix/2618
Registro completo de metadados
Campo DCValorIdioma
dc.contributor.advisor1Christophe Saint-Christie de Lima Xavier-
dc.creatorRomario Lira Batista-
dc.date.accessioned2016-09-23T15:20:30Z-
dc.date.available2016-09-23T15:20:30Z-
dc.date.issued2012-07-31-
dc.identifier.urihttp://riu.ufam.edu.br/handle/prefix/2618-
dc.description.resumoNos 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.pt_BR
dc.description.sponsorshipFAPEAMpt_BR
dc.formatPDF-
dc.languagept_BRpt_BR
dc.publisherUniversidade Federal do Amazonaspt_BR
dc.publisher.countryBrasilpt_BR
dc.publisher.departmentInstituto de Ciências Exatas e Tecnologia - Itacoatiarapt_BR
dc.publisher.programPROGRAMA PIBIC 2011pt_BR
dc.publisher.initialsUFAMpt_BR
dc.rightsAcesso Abertopt_BR
dc.subjectRedes de Petri-
dc.subjectCompiladores-
dc.subjectPrototipação-
dc.subject.cnpqCIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWAREpt_BR
dc.titleEspecificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcadospt_BR
dc.typeRelatório de Pesquisapt_BR
dc.pibic.cursoEngenharia de Softwarept_BR
dc.pibic.nrprojetoPIB-E/0149/2011-
dc.pibic.projetoEspecificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados-
dc.pibic.dtinicio2011-08-01-
dc.pibic.dtfim2012-07-31-
Aparece nas coleções:Relatórios finais de Iniciação Científica - Ciências Exatas e da Terra

Arquivos associados a este item:
Arquivo TamanhoFormato 
PIB_E_0149_2011.pdf1,34 MBAdobe PDFVisualizar/Abrir
Mostrar registro simples do item Recomendar este item


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