Verificação de propriedades de diagramas de atividade em um ambiente de modelagem aberto com suporte a rastreabilidade

Abstract

As technology advances, models and systems become increasingly complex, as does the effort to verify them. As a project progresses, the cost of correcting errors increases exponentially. Thus, techniques that help identify such errors in advance are increasingly important. Among these techniques, model checking has been presented as a interesting approach. Nevertheless, it requires manipulation of formal notations that are difficult to operate by system designers. Therefore, the creation of tools that abstract the formal aspects of these verification approaches has been shown as a promising way forward. Another relevant aspect is that some problems may arise due to the concurrent nature of these systems. Problems such as deadlock and non-determinism are quite present in this perspective. However, most of the current tools lack the capability to handle such problems. In addition, those that succeed are often tools that require paid licenses. In this work, we expand the tool created in previous works so that it can be used in open modeling environments, while still being open source and non-commercial. Our tool now has the ability to verify properties such as deadlock and non-determinism of activity diagrams that are created using the SysML language in an open modeling environment called OpenMBEE. Although some other works perform deadlock verification, few are those that perform non-determinism verification, even fewer are those that can perform both. Our tool has an underlying formal mechanization that allow us to perform automated checks. Furthermore, the tool also brings the advantage to its users that they do not need to understand or manipulate such a formal language, because we provide a traceability module that track the results of the formal verification back to the modeling environment notation, which is based on the JSON format. The main contributions of this work are the increase in the expressiveness of the tool and the addition of support for the verification of activity diagrams of an open modeling environment. We evaluate our approach using a real industry model related to the development of a Thirty-Meter Telescope (TMT), which is provided by the OpenMBEE community.