Formal verification of a hybrid machine learning-based fault prediction model in Internet of Things applications

By increasing the complexity of the Internet of Things (IoT) applications, fault prediction become an important challenge in interactions between human, and smart devices. Fault prediction is one of the key factors to achieve better arranging the IoT applications. Most of the current research studies evaluated the fault prediction methods using simulation environments. However, formal verification of the correctness of a fault prediction method has not been reported yet. This paper presents a behavioral modeling and formal verification of a hybrid machine learning-based fault prediction model with Multi-Layer Perceptron (MLP) and Particle Swarm Optimization (PSO) algorithms. In particular, the PSO is used for feature selection. Then, the fault prediction is considered as a behavior to be verified formally. The fault prediction behavior is divided into two types of behaviors: dimension reduction behavior and prediction behavior. For each of the behaviors, one formal model is designed. The behavioral models designed are mapped into the Labeled Transition System (LTS). The Process Analysis Toolkit (PAT) model checker is employed to evaluate the behavioral models. The accuracy of the fault prediction method is done by some existing specifications such as deadlock-free and reachability properties in terms of linear temporal logic formulas. Also, the verification of the fault prediction behaviors is used to detect the defect metrics of information-centric IoT applications. Experimental results showed that our proposed verification method has minimum verification time and memory usage for evaluating critical specification rules than other research studies.