Deterministic Formal Modeling of Smart Lightening System using Internet of Things

A collection of sensors and actuators which sense data, process and communicate with each other via internet within a network is called Internet of things (IoT). Smart city is an integration of smart states, sensors and actuators implemented to sense data from real environment within a network. The sensors and actuators embedded in real scenario enables transformation of intelligent environment. Many researchers have developed different solutions for modeling of smart cities, but efficient systems are not addressed in terms of efficiency. However, we have focused on energy efficient smart lightening system which is an important component of a smart city. In our proposed model, we have divided street lights energy usage into three categories: low, moderate and high. The street light energy usage is low when there is a day light, moderate when there is no heavy traffic on roads and high when there is heavy traffic on roads. Street lights turn on when a vehicle enters in a passage after sensing its entry within a region. A passage is collection of sensors which detects a vehicle and turn on all lights of the passage based on Unified Modeling Language (UML) sequence diagram. The sequence diagram is further converted into Deterministic Finite Automata (DFA) by which validation of the model is done. The DFA model is transformed into a formal model using Vienna Development Method-Specification Language (VDM-SL). The proof of correctness is provided by using VDM-SL toolbox.