Publication

Abstract : Geetha Lekshmy, V.Kannimoola, Jinesh M.IoT systems consist of smart devices ranging from a simple surveillance camera to pacemaker and mission-critical rockets. Though these systems are designed and developed systematically, it may malfunction due to hidden bugs that are uncovered only after deployment. Model checking and run-time verification are well-established procedures in formal methods to ensure the correctness of systems. We combine both these methods together to guarantee that IoT systems deployed in critical scenarios are fail-safe. This work aims at creating an end-to-end verification framework for IoT systems. Our system consists of (1) a design-time model for MQTT protocol based on the system specification, (2) a run-time model extracted from the execution trace of MQTT implementation and (3) the essential features of systems described in the temporal logic specification. The correctness of these models are checked against the specification using model checking and run-time verification approaches.