Banca de DEFESA: GUSTAVO BORGES LUGOBONI

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : GUSTAVO BORGES LUGOBONI
DATA : 07/05/2021
HORA: 09:00
LOCAL: por participação remota (https://meet.google.com/iym-eioe-rvb)
TÍTULO:

Um método para simular e verificar Redes de Petri Aninhadas

PÁGINAS: 75
RESUMO:

O formalismo das redes de Petri tem sido estendido de várias maneiras para suportar recursos como 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 presente trabalho apresenta um panorama histórico que levou ao desenvolvimento das redes aninhadas e tem como objetivo fornecer um método que permita analisar o comportamento de uma rede de Petri aninhada preservando sua estrutura multicamadas.
Para este fim, por meio desta dissertação, foi proposto o uso de uma ferramenta de verificação de modelos usualmente aplicada à verificação de software multithread, o SPIN.
Em particular, as redes de Petri aninhadas foram modeladas a partir de uma proposta de extensão da PNML (Petri Net Markup Language - ISO15909-2), e traduzidas de forma automática em modelos de entrada para o verificador SPIN.
O resultado da tradução automática foi avaliado a partir da análise de propriedades de redes aninhadas baseadas em modelos que surgem principalmente de dois domínios de aplicação: os sistemas multiagentes e fluxos de trabalho.
Isso foi feito utilizando exemplos da literatura para avaliar a eficácia do método e comparar os resultados com outras iniciativas.

MEMBROS DA BANCA:
Presidente - Interno ao Programa - 3008507 - CARLA NEGRI LINTZMAYER
Membro Titular - Examinador(a) Externo à Instituição - KELLY ROSA BRAGHETTO - USP
Membro Titular - Examinador(a) Externo à Instituição - JOSÉ REINALDO SILVA - USP
Membro Suplente - Examinador(a) Externo ao Programa - 3009301 - VLADIMIR EMILIANO MOREIRA ROCHA
Membro Suplente - Examinador(a) Externo ao Programa - 1544284 - LUIS ALBERTO MARTINEZ RIASCOS