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
Notação BPMN, Business Process Modeling Notation (BPMN), Sistema
de Sistemas (SoS), Linguagem Pi-ADL, Coreografia.
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.