1. Universidade Federal do Rio Grande do Norte
2. BDTD - Biblioteca Digital de Teses e Dissertações
3. Programa de Pós-Graduação em Engenharia Elétrica e de Computação
4. PPGEE - Doutorado em Engenharia Elétrica e de Computação

Título:	Verificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)
Autor(es):	Araújo, Ricardo Wagner de
Orientador:	Medeiros, Adelardo Adelino Dantas de
Palavras-chave:	Verificação Formal;Sistema de Raciocínio Procedural;Redes de Petri Coloridas;Formal Verification;Procedural Reasoning System;Coloured Petri Nets
Data do documento:	2-Set-2005
Editor:	Universidade Federal do Rio Grande do Norte
Referência:	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.
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
URI:	https://repositorio.ufrn.br/jspui/handle/123456789/18574
Aparece nas coleções:	PPGEE - Doutorado em Engenharia Elétrica e de Computação

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