# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 7 Case Study: Temperature-Measuring System  
This section presents a short case study to demonstrate the previously introduced methodologies. As shown in Figure 5, our case study has four sensors (\(SSR\)s) and one collector (\(CLLTR\)). \(SSR\)s communicate ambient temperature (\(TMPRT\)) to the \(CLLTR\). The \(CLLTR\) records the \(SSR\) values in a database for future use. We offer a streamlined model for the suggested case study, composed of eight finite state machines, in Figure 6. On the one hand, each \(SSR\)'s activity is described as a distinct finite state machine with three nodes and three transitions: \(TMPRT\) measurements and \(TMPRT\) transmission to the \(CLLTR\), obtaining the \(CLLTR\)'s acknowledgment. On the other hand, the \(CLLTR\)'s behavior is provided as a result of four finite state machines. Additionally, each of these finite state machines has three nodes and three transitions: Receiving the \(TMPRT\) from the associated \(SSR\), storing the \(TMPRT\), and sending the \(SSR\) an acknowledg \begin{table}
\begin{tabular}{p{56.9 pt} p{113.8 pt} p{113.8 pt}} \hline
**Tool Name** & **Functionality** & **Advantages** \\ \hline \multirow{4}{*}{Test.AI} & & Generates and executes test cases. Analyzes user behavior to generate test cases covering the most-critical and -common use cases. Automatically detects and prioritizes defects based on severity. Provides a dashboard for easy defect tracking and management. Reduces time and effort required for test case creation and maintenance. \\ \cline{2-3}  & & Generates and maintains test cases. Automatically analyzes user behavior to generate test cases covering the most-critical and -common use cases. Provides a dashboard for easy defect tracking and management. Reduces time and effort required for test case creation and maintenance. \\ \hline \multirow{4}{*}{Testim} & & Generates and maintains test cases. Automatically analyzes user behavior to generate test cases covering the most-critical and -common use cases. Provides a dashboard for easy defect tracking and management. Reduces time and effort required for test case creation and maintenance. \\ \cline{2-3}  & & Provides automated \(TST_{NG}\) across multiple platforms and environments. Detects defects and vulnerabilities. Provides insights and recommendations for improving software quality. Offers a dashboard for easy defect tracking and management. Ensures complete test coverage. \\ \hline \end{tabular}
\end{table} 
Table 6: _Cont._  
Figure 5: Temperature-measuring system (TMS). Next, we describe how a number of optimization techniques improved the FV and formal-based \(TST_{\text{NG}}\) for this case study. We begin with the FV aspects:  
* Abstraction: At this level, it is quite simple to see that the various components of the system under consideration are described at a very high level. Additionally, many details are abstracted away, and the interactions between the various \(SSR\)s are not taken into account either. * Modularization and compositionality: The suggested system is represented as a network of eight finite state machines. Every finite state machine has three states and three transitions. By multiplying the products of these different finite state machines, we obtain a large finite state machine with around \(3^{8}=6501\) states. If we expand the number of \(SSR\)s to eight, the product's states might reach \(3^{16}=43,046,721\), which is a big quantity. This demonstrates the significance of studying modularization and compositionality in order to reduce the size of the models under consideration. * Symmetry detection: It is easy to observe how the various \(SSR\)s and \(CLLTR\) pieces play symmetric roles. As a result, the FV of the entire studied system may be simplified to the verification of the product of only two finite state machines: one for each of the four \(SSR\)s and one for each of the four collecting elements (as shown in Figure 7). Figure 6: A simplified model for the TMS.