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
Use este identificador para citar ou linkar para este item: https://repositorio.ufrn.br/handle/123456789/18574
Registro completo de metadados
Campo DCValorIdioma
dc.contributor.advisorMedeiros, Adelardo Adelino Dantas dept_BR
dc.contributor.authorAraújo, Ricardo Wagner dept_BR
dc.date.accessioned2015-03-03T15:08:46Z-
dc.date.available2015-02-23pt_BR
dc.date.available2015-03-03T15:08:46Z-
dc.date.issued2005-09-02pt_BR
dc.identifier.citationARAÚ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.urihttps://repositorio.ufrn.br/jspui/handle/123456789/18574-
dc.formatapplication/pdfpor
dc.languageporpor
dc.publisherUniversidade Federal do Rio Grande do Nortepor
dc.rightsAcesso Abertopor
dc.subjectVerificação Formalpor
dc.subjectSistema de Raciocínio Proceduralpor
dc.subjectRedes de Petri Coloridaspor
dc.subjectFormal Verificationeng
dc.subjectProcedural Reasoning Systemeng
dc.subjectColoured Petri Netseng
dc.titleVerificação formal automatizada para sistemas de raciocínio procedural (PRS) utilizando redes de petri coloridas (RPC)por
dc.typedoctoralThesispor
dc.publisher.countryBRpor
dc.publisher.initialsUFRNpor
dc.publisher.programPrograma de Pós-Graduação em Engenharia Elétricapor
dc.contributor.authorIDpor
dc.contributor.authorLatteshttp://lattes.cnpq.br/4189661112532670por
dc.contributor.advisorIDpor
dc.contributor.advisorLatteshttp://lattes.cnpq.br/6787525856497063por
dc.contributor.referees1Botelho, Sílvia Silva da Costapt_BR
dc.contributor.referees1IDpor
dc.contributor.referees1Latteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4723628Z9por
dc.contributor.referees2Dórea, Carlos Eduardo Trabucopt_BR
dc.contributor.referees2IDpor
dc.contributor.referees2Latteshttp://lattes.cnpq.br/0143490577842914por
dc.contributor.referees3Alsina, Pablo Javierpt_BR
dc.contributor.referees3IDpor
dc.contributor.referees3Latteshttp://lattes.cnpq.br/3653597363789712por
dc.contributor.referees4Oliveira, Luiz Affonso Henderson Guedes dept_BR
dc.contributor.referees4IDpor
dc.contributor.referees4Latteshttp://lattes.cnpq.br/7987212907837941por
dc.description.resumoEste 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 algoritmospor
dc.publisher.departmentAutomação e Sistemas; Engenharia de Computação; Telecomunicaçõespor
dc.subject.cnpqCNPQ::ENGENHARIAS::ENGENHARIA ELETRICApor
Aparece nas coleções:PPGEE - Doutorado em Engenharia Elétrica e de Computação

Arquivos associados a este item:
Arquivo Descrição TamanhoFormato 
RicardoWA.pdf1,61 MBAdobe PDFThumbnail
Visualizar/Abrir
Mostrar registro simples do item


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