# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 4 Formal Methods
They provide a formal language for expressing mathematical statements and a set of rules for manipulating these statements to construct proofs. Proof assistants are useful for formalizing mathematical theories and verifying their correctness. They can also be used to verify the correctness of software and hardware designs. One of the main advantages of proof assistants is that they provide a high level of assurance that the proof is correct, since the proof is constructed using formal rules and the software checks the proof for correctness. * **Deductive verification [59]:** Deductive verification is a formal method used to verify the correctness of software by constructing a formal proof that the software satisfies its specifications. It works by starting with the specifications of the software and then systematically constructing a proof that the implementation of the software satisfies these specifications. Deductive verification is particularly useful for ensuring the correctness of safety-critical systems, such as those used in aviation and medical devices. One of the main advantages of deductive verification is that it can provide a high level of assurance that the software is correct, since the proof is constructed using formal rules and the proof can be checked by a computer. * **Design by refinement [60; 61]:** Design by refinement is a formal method used to develop correct software by iteratively refining an abstract specification of the software until a detailed implementation is obtained. It works by starting with a high-level specification of the software and then refining this specification step-by-step until a detailed implementation is obtained. Design by refinement can help to ensure that the software meets its specifications and is free of errors. It can also help to ensure that the software is maintainable and can be easily modified as requirements change. One of the main advantages of design by refinement is that it provides a systematic approach to software development, which can help ensure that the final product is correct and meets its specifications. * **Model-based testing (MBT) [62; 63]:** MBT is a formal method used to test software by generating test cases from a model of the software. It works by constructing a model of the software and then using this model to automatically generate test cases that exercise different parts of the software. MBT can help to ensure that the software meets its specifications and is free of errors. It can also help to reduce the time and effort needed to test the software. One of the main advantages of MBT is that it provides a systematic approach to \(TST_{\text{NG}}\) that can help to ensure that the final product is correct and meets its specifications. Table 2 summarizes these different types of formal methods, along with their advantages. Furthermore, formal methods can be classified into three categories: complete, partial, and asymptotically complete. In this classification, complete methods are guaranteed to provide a definitive answer to a given problem, while partial methods may not provide a definitive answer, but can provide useful information. Asymptotically complete methods are not guaranteed to find a solution, but as the problem size grows, the probability of finding a solution approaches 1. Here are some further details regarding these three classes:  
* **Complete methods [64]:** Complete methods are formal methods that are guaranteed to provide a definitive answer to a given problem. This means that, if a problem has a solution, a complete method will find it. For example, model checking is a complete method because it can systematically explore all possible behaviors of a system to determine whether a given property holds or not. Different types of complete FV exist, namely: SMT-based methods [65] and MILP-based methods. * **Partial methods [66]:** Partial methods are formal methods that may not provide a definitive answer to a given problem.