## 2 Materials and Methods
### Methodology--Development Process  
This section describes the steps and tools used during the experimentation (as seen in Figure 2). The methodology is simple, aiming at validating the hypothesis of adequate functioning and guaranteeing the following security aspects described in Table 6.  
In general, this study focuses on the dynamic and behavioral aspects of modeling the mechanism, leaving some static details outside its scope. The modeling workflow took place in four steps: (a) the modeling of the mechanism components; (b) abstract modeling with a state diagram of the mechanism's functioning; (c) modeling with timed automata; and (d) formal verification with temporal logic. In this manner, it was possible to trace the evolution of the modeling from the components and their messages to the formal verification. It is also observed that if any specialist wants to develop verification through another formal technique, it is possible to use the modeling from the STMs without any problems. This issue happens because the models are not dependent on any technology.  
Initially, the parts of the mechanism are presented through a **component diagram (a)**. This diagram expresses the communication between the software artifacts and where the components were deployed in each device (physical or virtual). Such information was used as an input to build the threat model and the other diagrams that follow.  
For **state modeling (b)**, the UML2 language was used. Specifically, the diagram of state machines was used, a behavioral diagram with which it is possible to analyze the life cycle of each component. Since these different software components are on different devices, they present great potential for interlocking. Due to this potential, this abstract overview becomes fundamental to error-free modeling.  
Employing **timed automata (c)**, the behavior and communication of each component expressed temporal characteristics. The state machines described in the previous step served as inputs to the TA construction process and underwent adaptations to alter the process' modeling in automata. Some aspects of STMs were suppressed in creating models that supported queries in temporal logic. It was also possible to implement guards (restrictions for the evolution of an automaton) and the simulation of the operation through the tool built into Uppaal ([[https://uppaal.org/](https://uppaal.org/)]([https://uppaal.org/](https://uppaal.org/)), accessed on 1 July 2023).  
Finally, there is the **property verification (d)**, which happened using temporal logic. The properties checked were derived from the security aspects mentioned above (Table 6). The queries were described in a TCTL reduction implemented in Uppaal and executed in the verification environment of this same tool.  
Upon the completion of the four steps, it was possible to present the entire proposed verification cycle. Additionally, it was also possible to describe each component and its behavior, convert behaviors into automata, and then verify the listed safety aspects.  
Figure 2: Steps to develop the study for formal verification of the proposal—existing artifacts are shown in red; steps developed and reported in this study are shown in green; artifacts produced as a result of these steps are shown in blue; and the final result of the work is shown in purple.