Um método para simular e verificar Redes de Petri Aninhadas
O formalismo das redes de Petri tem sido estendido de várias maneiras para suportar e.g. tipos
de dados, hierarquias, tempo, comunicação, prioridades, aninhamento e recursão. Os dois últimos
recursos combinados nas redes de Petri aninhadas permitem uma modelagem incremental usando
múltiplas camadas que é muito conveniente para lidar com os sistemas cada vez mais complexos de
hoje. Apesar disso, atualmente não existe ferramenta para projetar, simular e verificar as propriedades
dessas redes. Portanto, na prática, elas devem ser transformadas em redes hierárquicas de uma
única camada antes de serem analisadas. Esse processo de achatamento aumenta significativamente
o tamanho da rede, dificultando a simulação e a interpretação dos resultados no modelo original
após a verificação.
O objetivo deste projeto é fornecer um método que permita analisar o comportamento de uma
rede de Petri aninhada preservando sua estrutura multicamadas. Para este fim, o projeto propõe o
uso de ferramentas de verificação de modelos usualmente aplicadas à verificação de software. Em
particular, as redes de Petri aninhadas serão modeladas em Renew e traduzidas de forma automática
em modelos de entrada para o verificador SPIN. No projeto será construído um benchmark de
redes aninhadas baseadas em modelos que surgem principalmente de dois domínios de aplicação:
os sistemas multi-agentes e fluxos de trabalho. Outros exemplos da literatura serão usados para
avaliar a eficácia do método e comparar os resultados com outras iniciativas.