Banca de DEFESA: LEILA DE CARVALHO COSTA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
DISCENTE : LEILA DE CARVALHO COSTA
DATA : 14/09/2021
HORA: 09:00
LOCAL: webconferencia
TÍTULO:

VERIFICAÇÃO FORMAL DE SISTEMAS DE SISTEMAS (SOS) MODELADOS EM DIAGRAMAS DE COREOGRAFIA (BPMN)

PARA DETECÇão PRÉVIA DE ERROS TIPICOS DE TEMPO DE EXECUçÃO

PALAVRAS-CHAVES:

Notação BPMN, Business Process Modeling Notation (BPMN), Sistema

de Sistemas (SoS), Linguagem Pi-ADL, Coreografia.

PÁGINAS: 65
RESUMO:

Sistema de Sistemas (SoS) são compostos por um conjunto de sistemas, que interagem entre si

para um objetivo comum. Assim, ele tende a ser maior e mais complexo do que os sistemas

tradicionais. Para abordar a questão da complexidade inerente a este tipo de sistemas

complexos, eles são frequentemente modelados usando a Business Process Modeling and

Notation (BPMN), que é uma notação padrão para modelagem de processos de negócios.

O diagrama de coreografia, introduzido na versào BPMN2.0, fornece conceitos adequados

para representar as interações entre os sistemas constituintes de um SoS. No entanto,

os modelos criados com essa notação podem conter erros, alguns dos quais podem ser

detectados em tempo de design e outros apenas em tempo de execução. Os erros de

sintaxe são facilmente detectados com o auxílio de ferramentas de modelagem, no entanto,

a ausência de uma semântica formal para BPMN torna mais difícil identificar erros de

tempo de execução, como por exemplo, deadlocks, livelocks e outras propriedades de

seguran¸ca em diagramas de coreografia de BPMN. Esses erros são difíceis de detectar e

podem levar a uma operação inadequada ou até mesmo ao travamento do sistema. Nesse

contexto, um método para identificar erros de tempo de execução consiste em traduzir

o diagrama BPMN em um modelo formal que pode ser analisado em um verificador

de modelo. Assim, apresentamos uma abordagem para construir um modelo formal

para os diagramas de coreografia de BPMN em termos da linguagem formal PI-ADL,

que é uma linguagem projetada para a especificação de arquiteturas dinâmicas, uma

caracteríıstica intríınseca dos SoS. Portanto, definimos o mapeamento dos elementos do

diagrama de coreografia para pi-ADL, a fim de auxiliar sua descrição formal em pi-ADL.

Tais modelos pi-ADL permitem sua verificação formal por meio de um verificador de

modelo específico, possibilitando assim, a detecção prévia de erros em tempo de execução

no sistema modelado.

MEMBROS DA BANCA:
Presidente - 1708274 - RITA SUZANA PITANGUEIRA MACIEL
Interna - 1678446 - LAIS DO NASCIMENTO SALVADOR
Externo à Instituição - FLAVIO OQUENDO - UBS