Formal Specification Ensuring Security at Entrance and Exit of Smart Parking System

The IoT (Internet of Things) is an essential technology for the advancement of smart cities. IoT allows different objects to link and exchange information between them. A smart parking system is a key element in the development of the smart cities that solves numerous parking difficulties such as road congestion, time waste, fuel consumption, and insecurity of cars at parking places. In this paper, a smart car parking system based on IoT is described through several methods such as UML, automata, and VDM-SL (Vienna Development Method-Specification Language). Unified Modeling Language (UML) is employed to visualize the design and requirements of the system model. The automata theory is utilized to describe the behavior of the mechanism, which searches valid and free parking spaces based on information collected from IoT objects. The functionality of the system includes searching of legitimate free parking slots, reservation of slots, update and cancelation of reservation, and security of entrance and exit points of the parking area. The system has been converted into formal methods using VDM-SL and for the validation and verification, it is analyzed through the VDM-SL toolkit.