Relatório de Pesquisa

Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados

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, p...

ver descrição completa

Autor principal: Romario Lira Batista
Grau: Relatório de Pesquisa
Idioma: pt_BR
Publicado em: Universidade Federal do Amazonas 2016
Assuntos:
Redes de Petri
Compiladores
Prototipação
CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
Acesso em linha: http://riu.ufam.edu.br/handle/prefix/2618
id oai:localhost:prefix-2618
recordtype dspace
spelling oai:localhost:prefix-26182025-03-10T20:26:08Z Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados Romario Lira Batista Christophe Saint-Christie de Lima Xavier Redes de Petri Compiladores Prototipação CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE 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. FAPEAM 2016-09-23T15:20:30Z 2016-09-23T15:20:30Z 2012-07-31 Relatório de Pesquisa http://riu.ufam.edu.br/handle/prefix/2618 pt_BR Acesso Aberto PDF Universidade Federal do Amazonas Brasil Instituto de Ciências Exatas e Tecnologia - Itacoatiara PROGRAMA PIBIC 2011 UFAM
institution Repositório Institucional - Universidade Federal do Amazonas
collection RI-UFAM
language pt_BR
topic Redes de Petri
Compiladores
Prototipação
CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
spellingShingle Redes de Petri
Compiladores
Prototipação
CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
Romario Lira Batista
Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
topic_facet Redes de Petri
Compiladores
Prototipação
CIÊNCIAS EXATAS E DA TERRA: ENGENHARIA DE SOFTWARE
description 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.
author_additional Christophe Saint-Christie de Lima Xavier
author_additionalStr Christophe Saint-Christie de Lima Xavier
format Relatório de Pesquisa
author Romario Lira Batista
title Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
title_short Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
title_full Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
title_fullStr Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
title_full_unstemmed Especificação executável usando uma Linguagem de Redes de Petri colorida no Domínio de Sistemas Embarcados
title_sort especificação executável usando uma linguagem de redes de petri colorida no domínio de sistemas embarcados
publisher Universidade Federal do Amazonas
publishDate 2016
url http://riu.ufam.edu.br/handle/prefix/2618
_version_ 1831969287786463232
score 11.755432

Registros relacionados