# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 4 Formal Methods  
In this section, we provide a concise overview of the most-prevalent forms of formal techniques currently available to the research community [15; 16] (Figure 2):  
* **Abstract interpretation [53]:** Abstract interpretation is a formal method used to analyze and verify the behavior of computer programs. It is a technique that involves approximating the behavior of a program by abstracting away some of its details. The goal of abstract interpretation is to prove that a program satisfies certain properties, such as safety, liveness, or termination. Abstract interpretation works by defining a set of abstract values that represent the possible states of a program. These abstract values are defined in such a way that they over-approximate the set of possible concrete values. This allows abstract interpretation to reason about the behavior of a program without actually executing it. One of the key benefits of abstract interpretation is that it can be used to analyze programs that are too complex to be analyzed using other methods. This is because abstract interpretation can reason about the behavior of a program at a higher level of abstraction, which makes it possible to handle a much larger state space. * **Semantic static analysis [54]:** Semantic static analysis is a formal method used to analyze the behavior of computer programs by examining their source code. The goal of semantic static analysis is to detect errors and potential problems in a program before it is executed. Semantic static analysis works by analyzing the syntax and structure of a program to infer its meaning. This is done by constructing a mathematical model of the program's behavior, which can then be used to reason about its properties. One of the advantages of semantic static analysis is that it can be applied early in the development process, which can save time and resources. By detecting errors before a program is executed, semantic static analysis can help to ensure that the final product is correct and reliable. However, semantic static analysis can be challenging because it relies on the ability to reason about complex mathematical models of program behavior. This requires specialized knowledge and expertise in formal methods and mathematical analysis. Additionally, the accuracy of semantic static analysis depends on the quality of the model used, which can be difficult to construct for complex programs [55; 56]. * **Model checking [57]:** Model checking is a formal method used to verify the correctness of a system by exhaustively exploring its possible behaviors. It works by constructing a model of the system and specifying the desired properties that the system should satisfy. The model checker then systematically explores all possible states of the system to determine whether these properties hold for all possible behaviors. Model checking is particularly useful for verifying complex systems, such as concurrent and distributed systems, where traditional \(TST_{NG}\) methods may not be sufficient. It can also be used to verify hardware designs and protocols. One of the main advantages of model checking is that it can provide complete coverage of all possible behaviors, making it a powerful tool for ensuring the correctness of critical systems. \begin{table}
\begin{tabular}{l l l l} \hline \hline
**Layer** & **Function** & **Examples** & **Protocols** \\ \hline Perception & Data collection & Sensors, actuators & Zigbee, WiFi, Bluetooth \\ \hline Network & Communication & Cellular, satellite, ad hoc & TCP/IP, MQTT, CoAP \\ \hline Middleware & Data management & Data brokers, message queues & AMQP, MQTT, DDS \\ \hline Application & Service provision & Smart homes, healthcare monitoring & REST, SOAP, CoAP \\ \hline \hline \end{tabular}
\end{table} 
Table 1: Layers, functions, examples, and protocols of the IoT. * **Proof Assistants [58]:** Proof assistants are software tools that help users construct and verify mathematical proofs.