oa Application Of Design For Verification To Smart Sensory Systems

Wireless Sensor Networks (WSNs) have unleashed researchers and developers to propose a series of smart systems that serve the needs of societies and enhance the quality of services. WSNs consist of a set of sensors that sense the environmental variables, such as temperature, humidity, speed of objects, and report them back to a central node. Although such architecture seems simple, it is lack of many limitations that might affect its scalability, modularity of coded programs, and correctness in terms of synchronization problems such as nested monitor lockouts, missed or forgotten notifications, or slipped conditions. This research investigated the application of design for verification approach in order to come with a design for verification framework that takes into account the specialized features of smart sensory systems. Such contribution would facilitate 1) verifying coded programs to detect temporal and concurrent problems, 2) automating the verification process of such complex and critical systems, and 3) modularizing the coding of these systems to enhance their scalability. Our proposed framework relies on separating the design of the system's interfaces from the coded body; separation of concerns. For instance, we are not looking for recompiling the coded programs but, instead, we are looking for discovering design errors resulted from the concurrent temporal interactions among different programming objects. For this reason, our proposed framework adapts the concurrency controller design pattern to model the interactions modules. As a result, we were able to study the interactions among different actions and automatically recognize the transitions among them. Therefore, such recognition guarantees building a finite-state automaton that formulate the input description to a model-checker to verify some given temporal properties. To evaluate our proposed methodology, we have verified a real-time smart irrigation system that consists of a set of different sensors, which are controlled by a single controller unit. The system has already installed at our research field to control the irrigation process for the purpose of saving water. Further, we designed a set of specifications, temporal specifications, to check whether the system confirms to these specification during the interactions among heterogeneous sensors or not. If not, the model-checker returns a counter example of a sequence of states that violate a given specification. Thus, the counter example would be a great gift to fix the design error, which would minimize the risk of facing such error during run-time. The results showed that applying the proposed framework facilitates producing scalable, modular, and error-free sensory systems. The framework allowed us to detect critical design errors and fix them before deploying the smart sensory system. Finally, we also were able to check the power consumption model of our installed sensors and the effect of data aggregation on saving more power during future operations.