# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 1 Introduction  
The Internet of Things (IoT) has become an indispensable part of modern life, connecting billions of devices to the Internet and enabling seamless connectivity, automation, and real-time monitoring [1; 2; 3; 4]. The IoT has transformed various industries, including healthcare, transportation, smart homes, and industrial automation, resulting in significant improvements in efficiency, productivity, and convenience [5; 6; 7; 8]. However, the weaknesses of IoT systems, such as limited resources, heterogeneous devices, and a lack of standardization, make them prone to dangerous faults and attacks [9; 10; 11; 12]. These vulnerabilities have resulted in significant losses and damages in the past. For example, in 2016, the Mirai botnet attack exploited the security weaknesses of IoT devices to launch a massive distributed denial-of-service (DDoS) attack, which disrupted the Internet across the globe. The attack caused an estimated USD 323,000 loss per hour for the affected companies, totaling over USD 100 million in damages [13]. Another example is the Stuxnet worm, which targeted industrial control systems and caused physical damage to nuclear centrifuges in Iran. The attack is estimated to have set back Iran's nuclear program by two years and caused over USD 1 billion in damages [14]. To ensure the reliability, security, and safety of IoT systems, it is crucial to apply FV&V techniques. Formal methods use mathematical techniques to model and analyze systems rigorously [15; 16; 17]. As illustrated in Figure 1, they allow system designers to specify the behavior and properties of the system using precise mathematical notations, such as logic formulas and state machines. Formal methods can then use automated tools to analyze the system's behavior and properties, such as checking for consistency, completeness, and correctness [18]. They can also identify potential errors, vulnerabilities, and attacks by exploring the system's behavior under different scenarios [19]. Formal methods can help detect design errors early in the development process and ensure that the system meets the specified requirements and standards. Testing (\(TST_{NG}\)) is an essential step in the verification and validation process, and various techniques have been proposed to test IoT systems effectively [20; 21; 22]. For example, model-based testing (MBT) techniques generate test cases automatically from a formal model of the system, which can help achieve better test coverage and reduce the \(TST_{NG}\) effort [23; 24; 25]. Fuzzy \(TST_{NG}\) techniques generate random input data to stress-test the system and identify vulnerabilities and edge cases [26; 27]. Moreover, hardware-in-the-loop \(TST_{NG}\) techniques can test the interaction between the software and the hardware components of IoT systems, which can help detect integration issues and compatibility problems [28; 29; 30]. The need for formal method verification arises from the criticality of ensuring the reliability and security of IoT systems, which are often deployed in safety-critical domains such as healthcare, transportation, and industrial control. FV&V techniques provide a systematic approach to verifying the correctness of these systems by mathematically modeling their behavior and rigorously verifying that they meet their specifications. While FV&V techniques can be time-consuming, they can also reduce the overall cost of development by identifying and eliminating potential issues early in the design process. Moreover, the use of automated tools and techniques can help reduce the manual effort required for FV&V, making it more applicable to meet time-to-market constraints. The application of updates and patches to IoT systems can potentially introduce new vulnerabilities or alter the behavior of the system. To address this, FV&V techniques can be used to verify the correctness of updates and patches before they are applied to the system. This can help ensure that the system remains reliable and secure even after updates and patches are applied.