FMS-Workflow Modeling Based on P-Timed Stochastic Petri Net  

作　　者：Walid Ben Mesmia Kamel Barkaoui Mohamed Escheikh Walid Ben Mesmia;Kamel Barkaoui;Mohamed Escheikh(Sys’Com-ENIT, Tunisia, ENIT, Le Belvédère, Tunis, Tunisia;CEDRIC-CNAM, Paris, France)

机构地区：[1]Sys’Com-ENIT, Tunisia, ENIT, Le Belvédère, Tunis, Tunisia [2]CEDRIC-CNAM, Paris, France

出　　处：《Journal of Software Engineering and Applications》2023年第9期443-482,共40页软件工程与应用（英文）

摘　　要：In this paper, we propose astochastic Petri net model P-timed Workflow (WPTSPN) to specify, verify, and analyze a business process (BP) of a Flexible Manufacturing System (FMS). After formalizing the semantics of our model, we illustrate how to verifysome of its properties (reachability, safety, boundedness, liveness, correctness, alive tokens, and security) in the P-Timed context. Next, we validate the relevance of the proposed model with MATLAB simulation through a specific FMS case study. Finally, we use a generalized truncated density function to predict the duration of a token’s sojourn (residence) in a timed place with respect to the sequence states of the global FMS workflow.In this paper, we propose astochastic Petri net model P-timed Workflow (WPTSPN) to specify, verify, and analyze a business process (BP) of a Flexible Manufacturing System (FMS). After formalizing the semantics of our model, we illustrate how to verifysome of its properties (reachability, safety, boundedness, liveness, correctness, alive tokens, and security) in the P-Timed context. Next, we validate the relevance of the proposed model with MATLAB simulation through a specific FMS case study. Finally, we use a generalized truncated density function to predict the duration of a token’s sojourn (residence) in a timed place with respect to the sequence states of the global FMS workflow.

关 键 词：WPTSPN SPN WORKFLOW FMS P-Timed Specification Verification Prediction 

分 类 号：O17[理学—数学]