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
| Identifer | oai:union.ndltd.org:IBICT/oai:repositorio.ufrn.br:123456789/18574 |
| Date | 02 September 2005 |
| Creators | Ara?jo, Ricardo Wagner de |
| Contributors | CPF: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 |
| Publisher | Universidade 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 Sets | IBICT Brazilian ETDs |
| Language | Portuguese |
| Detected Language | Portuguese |
| Type | info:eu-repo/semantics/publishedVersion, info:eu-repo/semantics/doctoralThesis |
| Format | application/pdf |
| Source | reponame:Repositório Institucional da UFRN, instname:Universidade Federal do Rio Grande do Norte, instacron:UFRN |
| Rights | info:eu-repo/semantics/openAccess |
Page generated in 0.0026 seconds