Verificação de Refinamento em Diagramas de Sequência com Estruturas de Controle

Abstract

The UML language offers several types of diagrams for system modeling, among themain behavioral diagrams is the sequence diagram. The sequence diagram can beused to model system use cases simply and visually. However, the UML language asa whole presents informal models that can only be verified by human experience. Thispaper refers to the continuation of a research line that aims to formalize UML sequence diagrams and perform refinement checks between diagrams.Here we propose aninitial version of a tool capable of translating UML sequence diagrams into CSP and perform-ing a refinement check using the FDR4 verifier. The differential point of this work isthe process of formalization of combined fragments that represent control structures insequence diagrams, here we will cover fragments such asoption,alternative, paralleland loop.