Verificação de modelos comportamentais UML como um serviço habilitando a aplicação de métodos formais ocultos.

Abstract

As systems become more complex, more effort is required to perform validations on them. In addition to complexity, the cost of corrections also increases as projects progress, making error detection at the earliest stages essential. Within Model-Based Systems Engineering, model verification is one of the possible approaches to solving the problem. However, performing such verification often involves the use of formal methods. These methods are complex and not all system designers are knowledgeable in them. Another important point is that, given the increasing need to support large loads, it is common to use concurrency in systems. This concurrent nature of systems brings with it the possibility of including problems such as deadlock and non-determinism, usually not verified by current tools, which often also require licenses for their use and offer little possibilities of integration with other tools and environments. In this sense, our work uses the framework built in previous initiatives to expand the possibility of checking models through free and open source microservices. Although other works have already performed the verification of properties in UML models, most of them depend on the installation of tools and allow little or no integration with other systems. Therefore, our main contribution is the construction of a microservices-based architecture to provide services for checking classic properties (deadlock and non-determinism) for a subset of behavioral UML models, more precisely activity diagrams and state machines.