Mapping Formal Results Back to UML Semi-formal Model

UML is a widely used modeling language and it has a semi-formal notation that helps the software developers with a set of modeling rules, but without the need to have expertise in formal methods. This semi-formalism encourages the use of UML in Software Engineering domain because the software engineers involved can understand UML diagrams easily. Whereas, formal methods are more accurate than UML and their formal models have a higher correctness than the UML models. Thanks to this correctness, over the years, researchers are seeking ways to assign a formal semantics to UML. Usually they focus on how to formalize UML diagrams, transform them into formal models (such as LISP) and use them in model checkers. However, few researches discuss the problem of how to present the formal results to an audience who has no knowledge of formal methods. In order to fulfil this problem, in this paper is presented a mapping responsible for making the correlation between the formal results and the UML semi-formal environment, allowing the developer to analyze the results without having advance knowledge of formal methods. Therefore, we hope that this work may contribute to the increased adoption of formal methods in the software development industry.