An Algebraic Approach to Modeling and Verifying Policy-Driven Smart Devices in IoT Systems

Internet of Things (IoT) is being widely adopted to facilitate living environments such as cities and homes to become smart. Devices in IoT systems are capable of automatically adjusting their behaviors according to the change of environments. The capability is usually driven by the policies which are predefined inside devices. Policies can be customized by end users. Inconsistencies or conflicts among policies may cause malfunction of systems and therefore must be eliminated before deployment. In this paper, we propose a novel algebraic approach to modeling and verifying policy-driven smart devices in IoT systems on the basis of a domain-specific modeling language called PobSAM (Policy-based Self-Adaptive Model) and an efficient rewriting system called Maude. We formalize the operational semantics of PobSAM using Maude, which is an executable specification as well as a formal verification tool. The Maude formalization can be used to verify smart devices that are specified in PobSAM. We conduct a case study on a smart home setting to evaluate the effectiveness and efficiency of our approach.