Learning and analysis of sensors behavior in IoT systems using statistical model checking

Analyzing the behavior of sensors is becoming one of the key challenges due to their increasing use for decision making in IoT systems. The paper proposes an approach for a formal specification and analysis of such behavior starting from existing sensor traces. A model that embodies the sensor measurements over time in the form of stochastic automata is built, then temporal properties are fed to Statistical Model Checker to simulate the learned model and to perform analysis. LTL properties are employed to predict sensors' readings in time and to check the conformity of sensed data with the sensor traces in order to detect any abnormal behavior. We also use LTL properties to analyze the collective behavior of a set of sensors and build a formal model that checks the conformity of a combination of sensors' readings in time.