Towards a reliable smart city through formal verification and network analysis

With the immense increase of population density, many challenges facing organizations and governments. Thus, it has become mandatory to turn up our cities to be intelligent by introducing IoT and smart grids to build smart buildings, smart communication technologies, smart healthcare systems, smart transportation, etc. Smart cities guarantee the healthy living of indoor inhabitants by sensing, processing and controlling all possible indoor–outdoor measures. In this paper, we develop a framework that systematically builds a reliable and secure Smart City Model (SCM) to be integrated then exploited by the building information model (BIM). SCM encloses both physical and digital models which highlight smart buildings in particular. First, the proposed solution identifies and models SCM components including their appropriate architectures that are responsible for communication, extension, information flow, and protection. To ensure SCM functional and security requirements, we develop a sound hybrid approach that relies on formal methods and network analysis. Uppaal model checker is used to verify the satisfiability of the smart city requirements whereas Cooja is deployed to simulate the connectivity and the communication coverage of the developed SCM. The obtained results, in Uppaal, showed that the different implemented scenarios are satisfying the functional correctness and security policies. Moreover, the simulation through Cooja showed that how different obstacles and positions of nodes affect the communication coverage and the energy consumption regarding the deployed nodes. Experimentally, the effectiveness of the developed framework has been shown through practical scenarios that are difficult to model and analyze.