Towards a Formal Verification of IoT System Models Designed in the Cisco Packet Tracer Tool

Abstract

The Cisco Packet Tracer (CPT) is a network and IoT systems design and simulation tool developed by Cisco Systems inc. The tool is widely used in academia and the industry to develop and simulate complex IoT systems for training purposes. Although the graphical notations of CPT are appealing to system developers, the tool does not support formal verification. Therefore, CPT is limited when it comes to the design and development of safety and secutiry critical IoT systems where faults can endanger people's lives or damage properties and businesses. This paper proposes a formal approach to the verification of IoT system models designed in the CPT tool, based on the Calculus of Context-aware Ambients (CCA). First, the graphical notations of CPT are mapped to processes in CCA that specify their behaviours. Then any desired property of a system can be specified as a Linear Temporal Logic (LTL) formula. Finally, the CCA Runtime Verification tool ccaRV is used to verify formally whether the behaviour of an IoT system model designed in CPT violates the system's requirements. The pragmatics of the proposed approach is illustrated using a case study.