# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 4 Formal Methods
This means that a partial method may not be able to determine whether a problem has a solution or not. For example, abstract interpretation is a partial method because it can provide an over-approximation of the behavior of a program, but it may not be able to determine whether the program satisfies a given property or not. * **Asymptotically complete methods:** Asymptotically complete methods are 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. This means that, for very large problems, an asymptotically complete method will almost always find a solution. For example, heuristic search is an asymptotically complete method because, as the size of the search space grows, the probability of finding a solution approaches 1, even though there is no guarantee that a solution will be found for any given problem instance. Table 3 summarizes these three classes of formal methods, along with their advantages and limitations. Complete methods provide a definitive answer, but may be computationally expensive and may not scale well to large problems. Partial methods can handle complex problems, but may not be able to detect all errors or find all solutions. Asymptotically complete methods can handle very large problems and can often find solutions quickly, but may not always find a solution and may not be able to guarantee correctness. Understanding the strengths and limitations of these different types of formal methods can help developers choose the most-appropriate method for their specific problem. \begin{table}
\begin{tabular}{p{113.8 pt} p{113.8 pt} p{113.8 pt}} \hline \hline
**Formal Method** & **Description** & **Main Benefits** \\ \hline Abstract Interpretation & \begin{tabular}{c} Analyzes and verifies the behavior of computer programs by abstracting away some details and approximating the program’s behavior \\ \end{tabular} & Can analyze complex programs and reason about their behavior at a higher level of abstraction \\ \hline Semantic Static Analysis & \begin{tabular}{c} Analyzes the behavior of computer programs by examining their source code and inferring their meaning \\ \end{tabular} & Can detect errors early in the development process and ensure the final product is correct and reliable \\ \hline Model Checking & \begin{tabular}{c} Verifies the correctness of a system by exhaustively exploring its possible behaviors \\ \end{tabular} & Provides complete coverage of all possible behaviors and can ensure the correctness of critical systems \\ \hline Proof Assistants & \begin{tabular}{c} Software tools that help users construct and verify mathematical proofs \\ \end{tabular} & Provides a high level of assurance that the proof is correct and can verify the correctness of software and hardware designs \\ \hline Deductive Verification & \begin{tabular}{c} Verifies the correctness of software by constructing a formal proof that the software satisfies its specifications \\ \end{tabular} & Provides a high level of assurance that the software is correct and can ensure the correctness of safety-critical systems \\ \hline Design by Refinement & \
\begin{tabular}{c} Develops correct software by iteratively refining an abstract specification of the software until a detailed implementation is obtained \\ \end{tabular} & Provides a systematic approach to software development that can ensure the final product is correct and meets its specifications \\ \hline MBT &
\begin{tabular}{c} Tests software by generating test cases from a model of the software \\ \end{tabular} & Can ensure the software meets its specifications and is free of errors and can reduce the time and effort needed to test the software \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Different types of formal methods. The most-important advantages of utilizing formal approaches are as follows:  
* **Abstraction:** Formal approaches allow abstraction, which means that they can provide a higher-level view of the software system.