## 4 Discussion  
This section presents some considerations, the secondary results, the results of each workflow step, and the simulation results. The secondary results were unexpected developments in this work, which are important for the conclusion and result. The results of each stage allowed us to follow the evolution of this work and verify its correctness throughout its development. Finally, the simulation results are the final results of the entire workflow, the result of evaluating the listed properties. Regarding the **considerations**, although there are different approaches to modeling and converting UML diagrams to [90; 91; 92] automata, we opted for manual conversion in this work. This conversion was carried out based on the life cycle projected by the states of the UML and expressed through the evolution of states in the AT. Some works prove the correctness of this method [93; 94], for example, through bisimulation between the converted models. This choice was based on the team experience capacity for choices during the desired conversion. Regarding the adoption of timed automata, this approach was necessary for quantifying some attempted actions during authentication (i.e., publications with invalid data). This type of quantification would bring additional complexity to other approaches, mainly in validating the desired properties in the model. Additionally, the correlated works reinforce and validate the importance of using timed automata for this situation. Although there are other highly relevant formalisms, such as Petri nets and colored Petri nets, the experience and set of previous works developed with TAs led us to adopt this approach in this study. Furthermore, ATs is a recursively enumerable language belonging to the same Chomsky classification for colored Petri nets [95], with the same expressiveness. Therefore, the choice of approach becomes a design decision only, and in this project, we decided to follow our expertise with TAs. Some **secondary results** are refinements of the state diagrams caused by the challenges encountered during the simulation. For example, in the simulation process, it was observed that the automaton went into dead-lock when the device was unauthenticated; yet, in some situations there was an interlock between sending data to the sensor and the mechanism. These challenges caused modifications to the STMs, leading to a modification to the ATs. As a result, the mechanism became deadlock-free. Another important secondary result was the verification and evaluation of the distributed nature of the mechanism's components. Through the simulation, it is possible to visualize the signaling between the various processes involved and prove the need for a formal verification that addresses temporal properties, such as the non-interlocking of the processes. As per **results of the workflow steps**, first, there is the section of **related works** where 20 different works were considered that used four different approaches of temporal logic for their accomplishment. Since most of the works were published in the last two years, it is possible to conclude that formal verification is a current and adequate tool for evaluating security solutions. This fact happens in a way that complements the security verification of protocols (i.e., AVISPA), going beyond the verification of information aspects and the availability (non-locking) of the proposed solutions. Analyzing the data from the related works, Figure 12(a),b, it is possible to access some important data. In regards to the annual distribution, Figure 12(a), the works are concentrated in the last two years (2020 and 2021), around 75% of all correlates. Still, on the annual distribution, the oldest work is from 2004 and uses LTL as the chosen approach. As for the approach used, Figure 12(b), TCTL has the largest number of correlated works. This data confirms this approach's importance for the formal verification of works related to the security area.