Formal Modeling and Verification of Scalable Process-Aware Distributed IoT Applications

IoT applications are distributed over multiple IoT computing and communicating resources across the network including but not limited to small devices, machines, and public clouds. These IoT applications are composed of clearly separated and communicating fragments that can be modeled as large scale business processes. Process fragments can be unique, deployed in one location such as the cloud. They can also be replicated over multiple locations, such as different rooms in a smart building. Formal modeling and verification of such business processes composed of replicated fragments is a challenging task. In this paper we present a formal approach of modeling and verification of IoT applications that takes into account the scalability and repeatability properties of process-aware IoT applications. We propose a concise way of modeling and a general framework for the verification that simplifies the burden of IoT application modeling and deployment.