Stepwise Verification for the BPMN With Timed and Stochastic Process Using a Colored Generalized Stochastic Petri Net

Internet of Things (IoT) technologies have been increasingly developed for real-time application in manufacturing processes to address heterogeneous devices and software effectively. Although almost all activities in a manufacturing process can perform an action when data objects arrive at the activity, physical devices or activities have process involving the operation of chance over time and probabilistic function for proceeding with their operations. Therefore, the formal verification of an IoT process design model have to consider the timed constraints, probabilistic tasks and dependencies between activities. This paper proposes a quantitative verification approach for analyzing and optimizing IoT manufacturing design models that are designed in business process model and notation (BPMN) representation. The transformation rules of BPMN element into the colored generalized stochastic Petri net (CGSPN) are proposed, and the stepwise approaches for refining and verifying the components of the CGSPN models are illustrated. Our framework helps the designers to automate the CGSPN model and to localize the operational gaps, time and flaws of the process manufacturing models.