Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)
| dc.contributor.advisor | Medeiros, Adelardo Adelino Dantas de | pt_BR |
| dc.contributor.advisorID | por | |
| dc.contributor.advisorLattes | http://lattes.cnpq.br/6787525856497063 | por |
| dc.contributor.author | Araújo, Ricardo Wagner de | pt_BR |
| dc.contributor.authorID | por | |
| dc.contributor.authorLattes | http://lattes.cnpq.br/4189661112532670 | por |
| dc.contributor.referees1 | Botelho, Sílvia Silva da Costa | pt_BR |
| dc.contributor.referees1ID | por | |
| dc.contributor.referees1Lattes | http://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4723628Z9 | por |
| dc.contributor.referees2 | Dórea, Carlos Eduardo Trabuco | pt_BR |
| dc.contributor.referees2ID | por | |
| dc.contributor.referees2Lattes | http://lattes.cnpq.br/0143490577842914 | por |
| dc.contributor.referees3 | Alsina, Pablo Javier | pt_BR |
| dc.contributor.referees3ID | por | |
| dc.contributor.referees3Lattes | http://lattes.cnpq.br/3653597363789712 | por |
| dc.contributor.referees4 | Oliveira, Luiz Affonso Henderson Guedes de | pt_BR |
| dc.contributor.referees4ID | por | |
| dc.contributor.referees4Lattes | http://lattes.cnpq.br/7987212907837941 | por |
| dc.date.accessioned | 2015-03-03T15:08:46Z | |
| dc.date.available | 2015-02-23 | pt_BR |
| dc.date.available | 2015-03-03T15:08:46Z | |
| dc.date.issued | 2005-09-02 | pt_BR |
| dc.description.resumo | 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 | por |
| dc.format | application/pdf | por |
| dc.identifier.citation | ARAÚJO, Ricardo Wagner de. Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC). 2005. 172 f. Tese (Doutorado em Automação e Sistemas; Engenharia de Computação; Telecomunicações) - Universidade Federal do Rio Grande do Norte, Natal, 2005. | por |
| dc.identifier.uri | https://repositorio.ufrn.br/jspui/handle/123456789/18574 | |
| dc.language | por | por |
| dc.publisher | Universidade Federal do Rio Grande do Norte | por |
| dc.publisher.country | BR | por |
| dc.publisher.department | Automação e Sistemas; Engenharia de Computação; Telecomunicações | por |
| dc.publisher.initials | UFRN | por |
| dc.publisher.program | Programa de Pós-Graduação em Engenharia Elétrica | por |
| dc.rights | Acesso Aberto | por |
| dc.subject | Verificação Formal | por |
| dc.subject | Sistema de Raciocínio Procedural | por |
| dc.subject | Redes de Petri Coloridas | por |
| dc.subject | Formal Verification | eng |
| dc.subject | Procedural Reasoning System | eng |
| dc.subject | Coloured Petri Nets | eng |
| dc.subject.cnpq | CNPQ::ENGENHARIAS::ENGENHARIA ELETRICA | por |
| dc.title | Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC) | por |
| dc.type | doctoralThesis | por |
Files
Original bundle
1 - 1 of 1