01. Universidade Federal Rural de Pernambuco - UFRPE (Sede)
URI permanente desta comunidadehttps://arandu.ufrpe.br/handle/123456789/1
Navegar
2 resultados
Resultados da Pesquisa
Item Verificação de modelos comportamentais UML como um serviço habilitando a aplicação de métodos formais ocultos(2022-10-04) Cavalcanti, Paulo Henrique Nascimento; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/7089611179473920As 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.Item Verificação de propriedades de diagramas de atividade em um ambiente de modelagem aberto com suporte a rastreabilidade(2022-05-27) Silva Filho, Renato Cavalcanti Domingues da; Lima, Lucas Albertins de; http://lattes.cnpq.br/0465071050875729; http://lattes.cnpq.br/4996480197238824As 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.