UML is considered a de facto standard software modeling language, offering a wide range of diagrams that provide engineers with a detailed view of various aspects of the modeled software.With the UML, it is possible to model business processes, data models, use cases, activities, user scenarios, among others, providing a high level of abstraction. Despite offering many types of diagrams, UML is not free from semantic inconsistencies, ambiguities, or inappropriate notations. Such problems end up creating misinterpretations of UML diagrams, becoming obstacles in the construction of reliable software and adoption of an architecture that is suitable for the project. One way to mitigate these gaps left by the UML is the use of formal methods, such as Petri Nets, for modeling systems. Using formal methods allows, among other advantages, to simulate

the behavior of the modeled system and analyze its properties. In addition, the use of formal methods helps in choosing the appropriate architectural components for the software, which satisfactorily meet your needs. In this dissertation, the formal method used to develop the models is the Time Petri Nets. For modeling an overview of the system, smaller models representing each microservice were modeled, and later joined using a bottom-up approach. To investigate in the literature which is the most used and most suitable type of Time Petri Nets, a systematic mapping was carried out on the state of the art of the last two decades (2001-2021), in which it was found that Petri Nets with time associated with its transitions are the most used. After the investigation, an industry case study was conducted in order to verify the behavior and analyze the properties of the models in Petri Nets with time associated with transitions on a microservices architecture.

Activity diagrams and UML Use Cases of the Electronic Document Management System were transcribed to diagrams in Petri Nets with time associated with their transitions. The system uses the microservices architecture, in which small services are implemented that perform a single task and communicate with each other through asynchronous messages. From transcribed models, their properties were analyzed and microservices behavior modeled in Time Petri Nets was verified. In addition, it was also possible to observe software timing problems and identify bottlenecks, which helped in the choice of appropriate architectural components for the software