# A Survey on Formal Verification and Validation Techniques for Internet of Things
## 2 Related Work  
In this section, we review several formal verification approaches proposed for IoT protocols in recent years, including the IoT Conflict Checker, trust-based service management, BiAgents*, and formal models of popular messaging protocols. We also discuss formal approaches to defining semantics for modeling IoT applications and ensuring physical layer security. Finally, we examine VerificationTalk, a mechanism for verifying device and network configurations to prevent incorrect deployment of IoT applications. The article [31] reviewed formal verification approaches for many IoT protocols. Formal verification is essential for early vulnerability detection, according to the report. The authors detailed the properties and approaches. An in-depth literature study identified four application fields: (1) functional checks, (2) security property checks, (3) ideas for better schemes including a priori security property checks, and (4) protocol implementation checks. The paper covered security properties and protocol tools. The authors also described typical model checks and discuss IoT difficulties and limitations. The fundamental contribution of [32] is the invention of a formal method approach, the IoT Conflict Checker (IoTC2), for ensuring the safety of controller and actuator behavior in the Internet of Things (IoT) in the face of conflicts. The work specified and implemented safety policies for controllers, actions, and triggering events in Prolog to demonstrate logical completeness and soundness. The Matlab Simulink Environment with its built-in Model Verification blocks was used to implement the detection policies. The authors used Simulink to develop a smart home environment and demonstrated how conflicts affect actions and the corresponding features. The method's scalability, efficiency, and accuracy  
Figure 1: A simplified diagram illustrating how formats methods function. were evaluated in a simulated environment, demonstrating its potential utility in real-world IoT applications. The work [33] represented and verified trust-based service management components in the Internet of Things (IoT) using a formal method based on higher-order logic (HOL). The study examined IoT service composition difficulties and trust-based alternatives, which outperform non-trust-based ones. The authors offered a trust and reputation system to identify appropriate service providers (SPs) for service composition plans and utilized HOL to validate the varied behaviors in the trust system and trust value computation procedures. Malicious nodes can skew trust value computation, leading in incorrect SP selection during service composition. The paper [34] proposed a Bigraphical Agents (BiAgents*) model to formalize the structure and behavior of Internet of Things (IoT) systems. While there has been much research on IoT networking and devices, formalizing and evaluating IoT systems is still in its infancy, according to the article. The BiAgents* specification is encoded in the Maude language to allow IoT systems to behave autonomously. An intelligent collision-avoidance system illustrated and evaluated the proposed approach. It formalizes and standardizes the intricate interactions between smart devices in the IoT ecosystem, making the article important. The primary result of the work [35] was the introduction of a timed message-passing process algebra-based formal model of the MQ Telemetry Transport (MQTT) Version 3.1 protocol. Modeling decisions were made, and inconsistencies in the original protocol specification were highlighted in this study. After performing a static analysis on the formal protocol model, the authors found that the protocol provided, at most, once and, at least, once delivery semantics to subscribers, as defined, for the first two QoS modes of operation. The authors, however, concluded that the third and highest QoS semantics were inaccurate in some respects and, at best, unclear in others. Finally, the authors proposed improving the protocol's QoS to that point.