Verificação formal de Sistemas de Sistemas (SoS) modelados em diagramas de coreografia (BPMN) para detecção prévia de erros típicos de tempo de execução.

Abstract

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 pi-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 pi-ADL, in order to obtain its formal description in pi-ADL. Such pi-ADL models allow its formal verification using a specific model checker, enabling the prior detection of runtime errors in the modeled system.