Return to search

Verifica??o formal automatizada para sistemas de racioc?nio procedural (PRS) utilizando redes de petri coloridas (RPC)

Made available in DSpace on 2015-03-03T15:08:46Z (GMT). No. of bitstreams: 1
RicardoWA.pdf: 1646499 bytes, checksum: efcc744c6ff7cea26befa0adbedb8c6a (MD5)
Previous issue date: 2005-09-02 / Este trabalho apresenta uma t?cnica de verifica??o formal de Sistemas de Racioc?nio Procedural, PRS (Procedural Reasoning System), uma linguagem de programa??o que utiliza a abordagem do racioc?nio procedural. Esta t?cnica baseia-se na utiliza??o de regras de convers?o entre programas PRS e Redes de Petri Coloridas (RPC). Para isso, s?o apresentadas regras de convers?o de um sub-conjunto bem expressivo da maioria da sintaxe utilizada na linguagem PRS para RPC. A fim de proceder fia verifica??o formal do programa PRS especificado, uma vez que se disponha da rede de Petri equivalente ao programa PRS, utilizamos o formalismo das RPCs (verifica??o das propriedades estruturais e comportamentais) para analisarmos formalmente o programa PRS equivalente. Utilizamos uma ferramenta computacional dispon?vel para desenhar, simular e analisar as redes de Petri coloridas geradas. Uma vez que disponhamos das regras de convers?o PRS-RPC, podemos ser levados a querer fazer esta convers?o de maneira estritamente manual. No entanto, a probabilidade de introdu??o de erros na convers?o ? grande, fazendo com que o esfor?o necess?rio para garantirmos a corretude da convers?o manual seja da mesma ordem de grandeza que a elimina??o de eventuais erros diretamente no programa PRS original. Assim, a convers?o automatizada ? de suma import?ncia para evitar que a convers?o manual nos leve a erros indesej?veis, podendo invalidar todo o processo de convers?o. A principal contribui??o deste trabalho de pesquisa diz respeito ao desenvolvimento de uma t?cnica de verifica??o formal automatizada que consiste basicamente em duas etapas distintas, embora inter-relacionadas. A primeira fase diz respeito fias regras de convers?o de PRS para RPC. A segunda fase ? concernente ao desenvolvimento de um conversor para fazer a transforma??o de maneira automatizada dos programas PRS para as RPCs. A convers?o autom?tica ? poss?vel, porque todas as regras de convers?o apresentadas seguem leis de forma??o gen?ricas, pass?veis de serem inclu?das em algoritmos

Identiferoai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18574
Date02 September 2005
CreatorsAra?jo, Ricardo Wagner de
ContributorsCPF:44418620400, http://lattes.cnpq.br/6787525856497063, Botelho, S?lvia Silva da Costa, CPF:72951028091, http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4723628Z9, D?rea, Carlos Eduardo Trabuco, CPF:55708245553, http://lattes.cnpq.br/0143490577842914, Alsina, Pablo Javier, CPF:42487455420, http://lattes.cnpq.br/3653597363789712, Oliveira, Luiz Affonso Henderson Guedes de, CPF:21929564287, http://lattes.cnpq.br/7987212907837941, Medeiros, Adelardo Adelino Dantas de
PublisherUniversidade Federal do Rio Grande do Norte, Programa de P?s-Gradua??o em Engenharia El?trica, UFRN, BR, Automa??o e Sistemas; Engenharia de Computa??o; Telecomunica??es
Source SetsIBICT Brazilian ETDs
LanguagePortuguese
Detected LanguagePortuguese
Typeinfo:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis
Formatapplication/pdf
Sourcereponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN
Rightsinfo:eu-repo/semantics/openAccess

Page generated in 0.0029 seconds