A context-aware framework formodelling and verification of smart parking systems in urban cities

摘要

Parking spaces have been considered as vital resources in urban areas. Finding parking spaces in jam-packed areas is often challenging, stressful, and uncertain for the drivers that causes traffic congestion with a consequent of wastage of time, fuel, and increase of pollution. In recent years, context-aware computing paradigm has been considered to be the most effective approach to address these kinds of issues. Context-aware systems acquire and understand contextual information according to the current situation, perform reasoning, and then act intelligently on behalf of the user. These applications often run on tiny resource-bounded smart devices with the incorporation of embedded or attached sensors on these devices and they often exhibit complex and adaptive behaviour. In this paper, we propose a context-aware parking application framework to assist drivers in finding parking slots dynamically while moving and/or arriving at the destination. We optimize the context-aware parking framework with bounds on computational resources for the decision support dynamically in a highly decentralized environment. To illustrate the use of the proposed system, we model the context-aware parking system using Uppaal model checker for formal analysis and verify the correctness properties of the system.