# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 2 Related Work
This work contributes significantly since it created a formal model of a popular messaging protocol and pinpointed ways in which its specification could be enhanced. The paper [36] proposed an MDE-based formal approach to define ThingML's formal semantics for modeling Internet of Things (IoT) applications. The variability of IoT components and communication protocols makes designing and developing them difficult. ThingML, a promising UML profile for these difficulties, lacks strict semantics, making it inappropriate for formal verification and analysis of system architectures [37]. Rewriting logic and Maude are used to build ThingML's formal semantics, implementing all concepts and behaviors. A program developed by the authors automatically converts ThingML specifications into Maude, enabling advanced analytical methods such as simulation and model testing. This work proposed a semantics mapping between ThingML ideas and Maude constructs, defined and implemented an operational semantics for the ThingML action language in Maude, and provided a case study. An Event-B proof-based formal model of Internet of Things (IoT) physical layer security and threats from requirements analysis to the goal level is the main contribution of the study [38]. The article underlined the need for security in IoT devices, especially those that generate, gather, or process sensitive data, and that preventing vulnerabilities is better than identifying them. The authors offered a three-step formal approach: building the IoT physical layer, checking for security weaknesses, and detecting physical layer assaults such as jamming and MAC spoofing. To demonstrate generalizability, an electrocardiogram (ECG) IoT system and a fire alarm system were used as case studies. The Rodin model-checking tool's proof responsibilities and ProB animator validated the authors' approach. This work's formal approach for IoT physical layer security and attack detection can assist in preventing security breaches and securing sensitive data. The proposed framework in [39] uses the Event-B formal technique to develop a safe Internet of Things (IoT) architecture and handle IoT security and privacy issues. The report noted that, while various novel IoT designs have been presented, they still face security and privacy issues, and formal verification can assist identify flaws early on. The authors used Event-B properties such as formal verification, functional checks, and model checkers to design formal spoofing attacks for the IoT environment and obtain IoT architecture accuracy by running simulations, proof obligation, and invariant checking. Formal verification, functional checks, and model checkers were used to validate IoT-EAA architecture models, which automatically fulfilled 82.35% of the proof responsibilities using Event-B provers. Finally, the study recommended a well-defined IoT security infrastructure to decrease IoT security issues. This study is important because it gives a formal way for developing a safe IoT architecture and resolving IoT security and privacy issues. The article [40] reviewed many Internet of Things (IoT) security challenges and proposed formal verification as a promising approach to detect flaws and guarantee security. Due to battery and processing limitations, IoT devices make online cyberattack detection difficult. The authors suggested pre-deploying the device with stricter security tests to reduce the attack surface. The study covered IoT security challenges such functional soundness, code errors, side-channel analysis, and hardware Trojans. State-of-the-art procedures use formal verification tools to detect vulnerabilities before device deployment. This paper is important since it reviews IoT device security vulnerabilities and presents formal verification as a solution. The VerificationTalk mechanism, which verifies device and network configurations to prevent incorrect deployment of Internet of Things (IoT) applications, is the key contribution of [41].