Formal Modeling and Verification of IoT-based Smart Transport System using SPIN Model Checker

Transportation systems that are intelligent are developing for the benefit of travelers. The transportation business has suffered greatly as a result of advanced technology like the Internet of Things (IoT). Ensuring the security of passengers and conserving their valuable time are the top priorities for various transportation networks. The system’s proper design is essential to transportation safety. This work uses the SPIN model checker to solve the issue of guaranteeing accuracy and upholding system safety. IOT-based smart transport systems have been the subject of much study, but formal verification to guarantee the accuracy of these systems has received less attention. This paper solves this issue by officially validating an SPIN-based transport system. Use the formal specification language, Process or Protocol Meta Language (PROMELA), to formally define the Internet of Things (IOT)-based smart transport system in this study. Using linear temporal logic (LTL) in the form of a formula, create a program graph for this process using the SPIN Model Checker and explain the safety and liveness features. By providing the program graph and LTL formulae as input to the SPIN model checker, which determines if the properties are met with the program graph, formal verification is carried out to guarantee accuracy.