Reliability Analysis of Smart Home Sensor Systems Based on Probabilistic Model Checking

With the rapid development of IoT in recent years, Smart Home, one of the IoT application markets, has also been gaining popularity. The emergence of Smart Homes has brought convenience to people's lives, especially for people who live alone with physical illness. Smart Home users normally have higher expectations for reliability and safety of sensor systems, particularly in light of how complicated and uncertain the living environment is. The present work attempts to propose a data-knowledge integrated solution to analyze, model and evaluate the reliability of sensor systems in a smart home by combining quantitative reliability analysis and probabilistic model checking. Probabilistic model checking techniques use logical reasoning to check quantitative properties (as system requirements) and provide mathematical guarantee for them. More specifically, Smart Home Sensor Systems (SHSS) is described as a Markov Chain, commonly used probabilistic model, which models the system behaviour (e.g., probabilistic choice of state transition), and SHSS reliability properties are defined by Probabilistic Computation Tree Logic (PCTL). These choices of model and specification formula allow us to use one of the most recently developed open source probabilistic model checkers, PRISM, to perform the model checking of reliability verification task in SHSS. A real world smart home dataset (Van Kasteren dataset) is employed along with PRISM to illustrate the modeling approach and demonstrate the feasibility and applicability of the proposed approach.