Formal Analysis of Human-Assisted Smart City Emergency Services

The concept of IoT-based Smart Cities has gained momentum in recent years. The research in this domain has focused on modeling key characteristics of future smart cities along with exploring their design and implementation aspects from multiple perspectives. There is, however, a lack of research effort to provide a holistic approach towards modeling smart city services. A comprehensive approach has to view the smart city as a dynamic, uncertain and complex environment where multiple events with varying severity occur in a continuous and non-deterministic manner. These events have to be handled efficiently with the available resources. In this paper, we present a holistic approach to model the probabilistic as well as non-deterministic aspects of the emergency management services of a smart city by using probabilistic model checking. Our proposed model captures the emergency events of varying severity occurring at several locations in a continuous and non-deterministic manner. These events are responded to by a smart emergency management unit (SEMU), which dispatches the required emergency response units (ERUs) to the event location. In addition to modeling a completely automated system, we introduce a human-assisted decision-making process in the model to reduce false alarms. The proposed model can be used to study and evaluate key parameters in designing a smart city emergency management system to meet given service level agreements. We have implemented our proposed model using the PRISM model checker and have conducted several case studies to highlight the effectiveness of our proposed approach for different scenarios of varying complexities.