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:

A method for simulating and verifying Nested Petri Nets

PÁGINAS: 75
GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Teoria da Computação
ESPECIALIDADE: Computabilidade e Modelos de Computação
RESUMO:

The Petri nets formalism has been adapted and extended in several ways in order to support features such as data structures, hierarchies, time, communication, priorities, nesting, and recursion.
The two last features, combined in the Nested Petri nets, allow incremental modeling by using multiple layers, which is very convenient for dealing with complex systems.
In spite of this, currently, there is no tool to simulate and verify the properties of these nets.
Therefore, in practice, these multilayer nets are usually turned into flat nets.
This flattening process increases significantly the size of the net, making the simulation and the interpretation of the results in the original model after verification difficult.

This work presents a historical overview that led to the development of nested networks and aims to provide a method that allows the analysis of the behavior of a nested Petri network while preserving its multilayer structure.
To that end, through this dissertation, the use of a model verification tool usually applied to multithreaded software verification, the SPIN, is proposed.
Particularly, the nested Petri nets were modeled in a proposed extension of the PNML (Petri Net Markup Language - ISO15909-2) that is automatically translated into input models for the SPIN verifier.
The result of this translation was evaluated by the analysis of some properties of nested networks based on models that arise mainly from two application domains: multiagent systems and workflows.
This was done using examples from the literature to assess the effectiveness of the method and to compare the results with other initiatives.

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