• Entrar
    Ver item 
    •   Página inicial
    • BIBLIOTECA DIGITAL: Teses & Dissertações
    • Teses & Dissertações
    • Ver item
    •   Página inicial
    • BIBLIOTECA DIGITAL: Teses & Dissertações
    • Teses & Dissertações
    • Ver item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Método para verificação de propriedades de redes de petri utilizando resolvedores SMT

    Thumbnail
    Visualizar/Abrir
    R - D - ANDERSON PEREIRA DAS NEVES.pdf (546.2Kb)
    Data
    2013
    Autor
    Neves, Anderson Pereira das
    Metadata
    Mostrar registro completo
    Resumo
    Resumo: Este trabalho apresenta um método para verificar as propriedades de alcançabilidade e de bloqueio em rede de Petri. Rede de Petri e um modelo formal utilizado para modelar sistemas. O metodo proposto consiste em representar uma propriedade da rede de Petri em uma instancia SMT, podendo entao submete-la a um resolvedor SMT, a fim de que o resultado desta resolucao defina se a rede tem a propriedade a ser verificada. O metodo proposto foi implementado e avaliado em um conjunto de redes de Petri. A modelagem apresenta como resultado as transicoes e o número de vezes que as mesmas sao disparadas, as marcacoes intermediarias e todos os estados da rede para cada disparo necessario para atingir um estado desejado. Durante os testes obteve-se tempos muito prúximos ao do sistema Lola que e uma ferramenta especifica para anAjlise de redes de Petri.
     
    Abstract: This work presents a method for verifying the properties of reachability and deadlock in Petri Net. Petri Net is a formal method used in systems modeling. The proposed method consists in represent properties of the Petri net in a SMT instance, then submit it to a resolver SMT, so that the result of this resolution set if the network has the property to be verified. The method proposed has been implemented and evaluated in a set of Petri nets. The results of this modeling presents the transitions and the number of times that they were shot, the markings and all intermediate states of the network for each shot needed to achieve a desired state. During tests times were obtained very close to the Lola system that is a specific tool for the analysis of Petri nets.
     
    URI
    https://hdl.handle.net/1884/32031
    Collections
    • Teses & Dissertações [10555]

    DSpace software copyright © 2002-2022  LYRASIS
    Entre em contato | Deixe sua opinião
    Theme by 
    Atmire NV
     

     

    Navegar

    Todo o repositórioComunidades e ColeçõesPor data do documentoAutoresTítulosAssuntosTipoEsta coleçãoPor data do documentoAutoresTítulosAssuntosTipo

    Minha conta

    EntrarCadastro

    Estatística

    Ver as estatísticas de uso

    DSpace software copyright © 2002-2022  LYRASIS
    Entre em contato | Deixe sua opinião
    Theme by 
    Atmire NV