NFA Based Formal Modeling of Smart Parking System Using TLA +

The smart objects are used to sense, communicate, send and to share information within a network. Everything which is connected directly or indirectly within a network for the sake of getting, analyze or interpreting data known as IoT. There are many proposed applications of IoT infrastructure in smart city. We have proposed model of smart parking system in this paper which is based on UML, automata-based model and formal methods. The depiction of real-world parking system is done in UML based models to indicate the flow and working of the system. Automata models are used to convert UML diagram into automated system which provides smart mechanism of parking system. Automated model of automata is represented in terms of states and transitions. Every state has unique identity and defined functionality. There are many operations of parking system which are modeled in this paper including find free spaces, search shortest path towards empty slot, car entrance and exit with in a region. A region is an area of parking system which is automated and use to sense a vehicle, car entrance, exit or to find a location. The formal method techniques are used to formally verify system properties using available facilities available in formal method tools. We have used Temporal Logic of Actions (TLA+) formal language to validate and verify system properties using formal techniques. TLA+ is mathematical based notation to describe a system using discrete mathematics concepts. We have integrated these three approaches to model parking system from depiction side, automation side and from the angle of verification and validation of the model.