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

Abstract

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.