# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 4 Formal Methods
This can help to manage complexity by hiding irrelevant details and focusing on the essential characteristics of the system. Abstraction also makes it easier to reason about the behavior of the system and to identify potential errors and defects. * **Bigorous analysis:** Formal methods provide a rigorous and systematic approach to analyzing software systems. This means that they use well-defined mathematical models and techniques to analyze the software, which can help to ensure that the analysis is accurate and complete. Rigorous analysis can identify defects and errors that may be missed by other methods, such as \(TST_{NG}\) or informal reviews. * **Early defect discovery:** Formal methods can be applied early in the software-development process, which can help to identify defects and errors before they become more difficult and expensive to fix. Early defect discovery can also help to improve the overall quality of the software and reduce the risk of defects, which could lead to system failures or safety hazards. * **Correctness guarantees:** Formal methods can provide correctness guarantees, which means that they can prove that the software meets its specifications and behaves correctly. This can provide a high level of assurance that the software is correct and \begin{table}
\begin{tabular}{p{56.9 pt} p{56.9 pt} p{56.9 pt} p{56.9 pt} p{56.9 pt}} \hline
**Class** & **Definition** & **Example** & **Advantages** & **Limitations** \\ \hline Complete Methods & Formal methods that are guaranteed to provide a definitive answer to a given problem & Model checking, theorem proving & Provide a definitive answer and can find all solutions & May be computationally expensive and may not scale well to large problems \\ \hline Partial Methods & Formal methods that may not provide a definitive answer to a given problem & Abstract interpretation, type checking & Can handle complex problems and can provide useful information even if a definitive answer cannot be found & May not be able to detect all errors or find all solutions \\ \hline Asymptotically Complete Methods & Formal methods that are not guaranteed to provide a definitive answer to a problem, but as the size of the problem grows, the probability of finding a solution approaches 1 & Heuristic search, stochastic methods & Can handle very large problems and can often find solutions quickly & May not always find a solution and may not be able to guarantee correctness \\ \hline \end{tabular}
\end{table} 
Table 3: Different classes of formal methods. Figure 2: Different types of formal techniques. reliable. Correctness guarantees are particularly important for safety-critical systems, where errors or defects could have serious consequences. * **Reliability:** Formal methods can improve the reliability of software systems by reducing the risk of errors and defects. This can help to ensure that the software behaves as expected and that it is robust and resilient to unexpected inputs or conditions. Reliability is particularly important for systems that need to operate continuously or that cannot be easily repaired or replaced. * **Efficient test scenarios:** Formal methods can help to identify the most-efficient test scenarios for a software system. This can reduce the time and effort needed to test the software, while still ensuring that the software meets its specifications and behaves correctly. Efficient test scenarios can also help to improve the overall quality of the software and reduce the risk of defects that could lead to system failures or safety hazards [62; 63]. * **Maintainability:** Formal methods can improve the maintainability of software systems by providing a clear and precise specification of the system's behavior. This can make it easier to modify or refactor the software without introducing errors or defects. Formal methods can also help to ensure that modifications do not violate the system's specifications or requirements.