Banca de DEFESA: LEILA DE CARVALHO COSTA

Uma banca de DEFESA de MESTRADO foi cadastrada pelo programa.
STUDENT : LEILA DE CARVALHO COSTA
DATE: 14/09/2021
TIME: 09:00
LOCAL: webconferencia
TITLE:

FORMAL VERIFICATION OF SYSTEMS OF SYSTEMS (SOS) MODELED IN BPMN CHOREOGRAPHY DIAGRAMS

- PREVIOUS DETECTION OF TYPICAL RUNTIME ERRORS

KEY WORDS:

Business Process Modeling Notation (BPMN), System of Systems (SoS),

⇡-ADL language, Choreography.

PAGES: 65
BIG AREA: Ciências Exatas e da Terra
AREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
SPECIALTY: Engenharia de Software
SUMMARY:

System of systems (SoS) is composed of a set of systems, which interact together for

a common goal. Thereby, it tends to be larger and more complex than traditional systems.

To address the question of the inherent complexity of this kind of complex systems,

they are frequently modeled using the Business Process Modeling and Notation (BPMN),

which is a standard modeling notation for business processes. The choreography diagram,

introduced in version BPMN 2.0, provides suitable concepts for representing the interactions

among constituents of a SoS. However, models created using this notation may

contain errors, some of which can be detected at design-time and others only at runtime.

Syntax errors are easily detected with the assistance of modeling tools. Nevertheless,

the absence of a formal semantics for BPMN makes it harder to identify runtime errors,

as for example, deadlocks, livelocks and other safety properties in BPMN choreography

diagrams. These errors are challenging to detect and may lead to an improper operation

or even a system lockup. In this context, a method for identifying runtime errors consists

of translating the BPMN diagram into a formal model that can be analyzed in a model

checker. Thereby we present an approach to build a formal model for the BPMN choreography

diagrams in terms of the formal language ⇡-ADL, which is properly designed for

the specification of dynamic architectures, an intrinsic characteristic of SoS. Therefore,

we define the mapping of the elements of the choreography diagram to ⇡-ADL, in order

to obtain its formal description in ⇡-ADL. Such ⇡-ADL models allow its formal verification

using a specific model checker, enabling the prior detection of runtime errors in the

modeled system.

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