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.
References
[1]
Alcacer, V. and Cruz-Machado, V. (2019) Scanning the Industry 4.0: A Literature Review on Technologies for Manufacturing Systems. Engineering Science and Technology, an International Journal, 22, 899-919. https://doi.org/10.1016/j.jestch.2019.01.006
[2]
(2020) CGP Gestion de Production. https://www.cours-gratuit.com/cours-gestion/cours-sur-les-outils-de-la-gestion-de-production
[3]
Courtois, A., Martin-Bonnefous, C. and Pillet, M. (2003) Gestion de production. 4 eme Edition, Editions d’Organization.
[4]
Ballarini, P., Barbot, B., Duflot, M., Haddad, S. and Pekergin, N. (2015) HASL: A New Approach for Performance Evaluation and Model Checking from Concepts to Experimentation. Performance Evaluation, 90, 53-77. https://doi.org/10.1016/j.peva.2015.04.003
[5]
Weske, M. (2019) Business Process Management: Concepts, Languages, Architectures. Springer, Berlin. https://doi.org/10.1007/978-3-662-59432-2_1
[6]
Van der Aalst, W.M.P. and Van Hee, K. (2002) Workflow Management: Models, Methods, and System. The MIL Press, Cambridge.
[7]
Ben Mesmia, W., Escheikh, M. and Barkaoui, K. (2020) DevOps Workflow Verification and Duration Prediction Using Non-Markovian Stochastic Petri Nets. Journal of Software: Evolution and Process, 33, e2329. https://doi.org/10.1002/smr.2329
[8]
Sbai, Z. and Barkaoui, K. (2012) Verification Formelle des Processus Workflow Collaboratifs. Conference francophone sur les Systemes Collaboratifs, (SysCo’12), 5, 197-200.
[9]
D’Ambrogio, A. and Zacharewicz, G. (2016) Resource-Based Modeling and Simulation of Business Processes. Proceedings of the 2016 Summer Computer Simulation Conference (SCSC 2016), Montreal, 24-27 July 2016, page.
(2020) Object Management Group Business Process Model and Notation. https://www.omg.org/spec/BPMN/2.0
[12]
(2020) BPMN 1.0 Business Process Model and Notation (BPMN)—Version 1.0 2020 URL. https://www.omg.org/spec/BPMN/1.1/PDF
[13]
Holzmann, G.J. (1997) The model checker SPIN. IEEE Transactions on Software Engineering, 23, 279-295. https://doi.org/10.1109/32.588521
[14]
(2020) BPMN 2.0 Business Process Modeling Notation. https://www.omg.org/spec/BPMN/2.0/
[15]
Kheldoun, A., Barkaoui, K. and Ioualalen, M. (2017) Formal Verification of Complex Business Processes Based on High-Level Petri Nets. Information Sciences, 385-386, 39-54. https://doi.org/10.1016/j.ins.2016.12.044
[16]
Ciardo, G. (1995) Discrete-Time Markovian Stochastic Petri Nets. In: Stewart, W.J., Ed., Computations with Markov Chains, Springer, Boston, 339-358. https://doi.org/10.1007/978-1-4615-2241-6_20
[17]
Bocciarelli, P., D’Ambrogio, A., Giglio, A., Paglia, E. and Gianni, D. (2014) Empowering Business Process Simulation through Automated Model Transformations. 2014 Proceedings of the Symposium on Theory of Modeling and Simulation—DEVS Integrative M&S Symposium, Tampa, 13-16 April 2014, 39-45.
[18]
Boucheneb, H. and Barkaoui, K. (2012) Parametric Verification of Time Workflow Nets. Proceeding of the 24th International Conference on Software Engineering and Knowledge Engineering SEKEC, San Francisco, 1-3 July 2012, 352-361.
[19]
Ben Mesmia, W., Escheikh, M. and Barkaoui, K. (2019) DevOps Workow Specification Based on Non-Markovian Stochastic Petri Nets with Enhanced Expressiveness. COSI’2019, Tizi-Ouzou, 24-26 June 2019, 2-12.
[20]
Yamaguchi, S., Yamaguchi, M. and Tanaka, M. (2008) A Soundness Verification Tool Based on the SPIN Model Checker for Acyclic Workflow Nets. The 23rd International Technical Conference on Circuits/Systems, Computers and Communications (ITC-CSCC 2008), Japan, 6-9 July 2008, 285-288.
[21]
Dumas, M., La Rosa, M., Mendling, J. and Reijers, H.A. (2018) Fundamentals of Business Process Management. Springer, Berlin. https://doi.org/10.1007/978-3-662-56509-4
[22]
Favrel, J. and Lee, K.H. (1985) Modelling, Analysing, Scheduling and Control of Flexible Manufacturing Systems. In: Falster, P. and Maxumder, R.B., Eds., Modelling Production Management Systems, Elsevier, Amsterdam, 279-288.
[23]
Cecil, J.A., Srihari, K. and Emerson, C.R. (1992) A Review of Petri-Net Applications in Manufacturing. The International Journal of Advanced Manufacturing Technology, 7, 168-177. https://doi.org/10.1007/BF02601620
[24]
Archetti, F. and Sciomachen, A. (1988) Representation, Analysis and Simulation of Manufacturing Systems by Petri-Net Based Models. In: Varaiya, P. and Kurzhanski, A.B., Eds., Discrete Event Systems: Models and Applications, Springer, Berlin, 162-178.
[25]
Cox, D.R. (1995) The Analysis of Non-Markovian Stochastic Processes by the Inclusion of Supplementary Variables. Mathematical Proceedings of the Cambridge Philosophical Society, 51, 433-440. https://doi.org/10.1017/S0305004100030437
[26]
Trivedi, K.S. and Kulkarn, V.G. (1993) FSPNs: Fluid Stochastic Petri Nets. In: Ajmone Marsan, M., Ed., ICATPN 1993: Application and Theory of Petri Nets 1993, Springer, Berlin, 24-31. https://doi.org/10.1007/3-540-56863-8_38
[27]
Ciardo, G., German, R. and Lindemann, C. (1994) A Characterization of the Stochastic Process Underlying a Stochastic Petri Net. IEEE Transactions on Software Engineering, 20, 506-515. https://doi.org/10.1109/32.297939
[28]
Krogh, B.H. and Srecnivas, R.S. (1987) Essenlially Decision Free Petri Nets for Real-Time Resource Allocation. Proceedings of 1987 IEEE International Conference on Robotics and Automation, Raleigh, 31 March-3 April 1987, 1005-1011.
[29]
Colter, S.M., Woodward, A.T., fluck, A.A., Smith, R. and White, D.M. (1986) Extended Petri-Nets: The Language of Factory Automation? Proceedings of ISATA 1986: 15th International Symposium on Advances in Technology Education, Croydon, 1-20.
[30]
Khansa, W., Aygalinc, P. and Denat, J.P. (1996) Structural Analysis of P-Time Petri Nets Computational Engineering in Systems Applications. CESA’96 IMACS Multiconference, Computational Engineering in Systems Applications, Lille, 9-12 July 1996, 127-136.
[31]
Calvez, S., Aygalinc, P. and Khansa, W. (1997) P-Time Petri Nets for Manufacturing Systems with Staying Times Constraints. IFAC Proceedings Volumes, 30, 1487-1492. https://doi.org/10.1016/S1474-6670(17)43571-3
[32]
Capkovic, F. (1995) A Petri Net-Based Approach to Synthesis of Control Systems for Discrete Event Dynamic Systems New Trends in Design of Control Systems 1994. Elsevier, 345-350.
[33]
DiLeva, A., Vernadat, F. and Bizier, D. (1987) Information Systems Analysis and Conceptual Database Design on Production Environments with M*. Computers in Industry, 9, 183-217. https://doi.org/10.1016/0166-3615(87)90037-6
[34]
Bruno, G. and Biglia, P. (1985) Performance Evaluation and Validation of Tool Handling in Flexible Manufacturing Systems Using Petri Nets. Proceedings of International Workshop on Timed Petri-Nets, Turin, July 1985, 64-71.
[35]
Balbo, G., Chiola, G., Franceschinis, G. and Roet, G.M. (1987) Generalised Stochastic Petri Nets for the Performance Evaluation of FMS. Proceedings of IEEE International Conference on Robotics and Automation, Raleigh, 31 March-3 April 1987, 1013-1018.
[36]
Narahari, Y. and Viswanadham, N. (1987) Performance Evaluation Using a Class of Petri-Nets with Deterministic and Exponential Firing Times. TENCON 87, 1987 IEEE Region 10 Conference: “Computers and Communications Technology toward 2000”, Seoul, 25-28 August 1987, 482-486.
[37]
Wadbwa, S. and Thrownc, J. (1988) Analysis of Collision Avoidance in Multirobot Cells Using Petri Nets. Robotersysteme, 4, 107-115. https://dblp.org/rec/journals/robotersysteme/WadhwaB88.bib
[38]
Martincz, J. and Silva, M. (1984) A Language for the Description of Concurrent System Modeled by Colored Petri Nets: Application to the Control of Flexible Manufacturing Systems. In: Chang, S.K., Ed., Languages for Automation, Springer, Boston, 369-388. https://doi.org/10.1007/978-1-4757-1388-6_18
[39]
Castelain, E., Corbel, D. and Gentina, J.C. (1985) Comparative Simulations of Control Processes Described by Petri-Nets. Proceedings of COMPINT 1985: Computer Aided Technologies, Quebec, 8-12 September 1985, 215-226.
[40]
Ammour, R., Leclercq, E., Sanlaville, E. and Lefebvre, D. (2017) Faults Prognosis Using Partially Observed Stochastic Petri Nets: An Incremental Approach. Discrete Event Dynamic Systems, 28, 247-267. https://doi.org/10.1109/WODES.2016.7497890
[41]
Ajmone Marsan, M., Balbo, G. and Conte, G. (1984) A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Transaction Computer Systems, 2, 93-122. https://doi.org/10.1145/190.191
[42]
Choi, I., Song, M., Park, C. and Park, N. (2003) An XML-Based Process Definition Language for Integrated Process Management. Computers in Industry, 50, 85-102. https://doi.org/10.1016/S0166-3615(02)00139-2
[43]
Lefebvre, D. (2017) Detection of Temporal Anomalies for Partially Observed Timed PNs. Mathematical Problems in Engineering, 2017, Article ID: 2821078. https://doi.org/10.1155/2017/2821078
[44]
Lefebvre, D. (2017) Probability of Faults for Partially Observed Timed PNs with Temporal Constraints. 2017 IEEE 14th International Conference on Networking, Sensing and Control (ICNSC), Calabria, 16-18 May 2017, 103-108. https://doi.org/10.1109/ICNSC.2017.8000075
[45]
Berthomieu, B. and Diaz, M. (1991) Modeling and Verification of Time Dependent Systems Using Time Petri Nets. IEEE Transactions on Software Engineering, 17, 259-273. https://doi.org/10.1109/32.75415
[46]
Choi, H. (1993) Performance and Reliability Modeling Using Markov Regenerative Stochastic Petri Nets. Ph.D. Thesis, Graduate School of Duke University, Durham.
[47]
Ciardo, G. and Lindemann, C. (1993) Analysis of Deterministic and Stochastic Petri Nets. Proceedings of 5th International Workshop on Petri Nets and Performance Models, Toulouse, 19-22 October 1993, 160-169.
[48]
Rachidi, S. (2019) Diagnostic des défauts dans les systèmes à évènements discrets soumis à des contraintes temporelles. Automatique/Robotique. Thèse de Doctorat, Normandie Université, Normandie, 26-30. https://tel.archives-ouvertes.fr/tel-02441760
[49]
Lefebvre, D., Rachidi, S., Leclercq, E. and Pigné, Y. (2018) Diagnosis of Structural and Temporal Faults for k Bounded Non-Markovian Stochastic Petri Nets. IEEE Transactions on Systems, Man, and Cybernetics: Systems, 50, 3369-3381.
[50]
Lefebvre, D., Rachidi, S., Leclercq, E. and Pigné, Y. (2018) Temporal Fault Diagnosis for k-Bounded Non-Markovian SPN. 2018 5th International Conference on Control, Decision and Information Technologies (CoDIT), Thessaloniki, 10-13 April 2018, 271-276. https://doi.org/10.1109/CoDIT.2018.8394843
[51]
Dugan, J., Trivedi, K., Geist, R. and Nicola, V.F. (1984) Extended Stochastic Petri Nets: Applications and Analysis. Performance’ 84: Proceedings of the Tenth International Symposium on Computer Performance Modeling, Measurement and Evaluation, Paris, 19-21 December 1984, 507-519.
[52]
Ajmone Marsan, M., Balbo, G., Bobbio, A., Chiola, G., Conte, G. and Cumani, A. (1989) The Effect of Execution Policies on the Semantics and Analysis of Stochastic Petri Nets. IEEE Transactions on Software Engineering, 15, 832-846. https://doi.org/10.1109/32.29483
[53]
Van Dongen, B.F., Crooy, R.A. and Van der Aalst, W.M.P. (2008) Cycle Time Prediction: When Will This Case Finally Be Finished? In: Meersman, R. and Tari, Z., Eds., On the Move to Meaningful Internet Systems: OTM 2008, Springer, Berlin, 319-336. https://doi.org/10.1007/978-3-540-88871-0_22
[54]
Andreas Rogge, S. and Mathias, W. (2015) Prediction of Business Process Durations Using Non-Markovian Stochastic Petri Nets. Information Systems, 54, 1-14. https://doi.org/10.1016/j.is.2015.04.004
[55]
WFMS (2020) Workflow Management System (WFMS). https://www.igi-global.com/dictionary/workflow-management-system-wfms/32777
Petri, C.A. (1962) Kommunikation mit Automaten (Communication with Automata). Ph.D. Thesis, University of Bonn, Bonn.
[58]
Muratat, T. (1989) Petri Nets: Properties, Analysis and Application. Proceedings of the IEEE, 77, 541-580. https://doi.org/10.1109/5.24143
[59]
Ramamoorthy, C.V. and Ho, G.S. (1980) Performance Evaluation of Asynchronous Concurrent Systems Using Petri Nets. IEEE Transactions on Software Engineering, SE-6, 440-449. https://doi.org/10.1109/TSE.1980.230492
[60]
Laftit, S. (1991) Graphes d’événements deterministes et stochastiques: Application aux systemes de production. Thèse de Doctorat, Université de Paris, Paris.
[61]
David, R. and Alla, H. (1992) Du grafcet aux reseaux de Petri. Hermes Science Publications, Paris.
[62]
Dicesare, F., Harhalakis, G., Proth, J.M., Silva, M. and Vernadat, F.B. (1993) Practice of Petri Nets in Manufacturing. Chapman et Hall, London. https://doi.org/10.1007/978-94-011-6955-4
[63]
Balbo, G. (2000) Introduction to Stochastic Petri Nets. In: Brinksma, E., Hermanns, H. and Katoen, J.P., Eds., EEF School 2000: Lectures on Formal Methods and PerformanceAnalysis, Springer, Berlin, 84-155. https://doi.org/10.1007/3-540-44667-2_3
[64]
Ballarini, P., Gallet, E., Le Gall, P. and Manceny, M. (2019) Formal Analysis of the Wnt/β-Catenin through Statistical Model Checking. In: Margaria, T. and Steffen, B., Eds., ISoLA 2014: Leveraging Applications of Formal Methods, Verification and Validation. Specialized Techniques and Applications, Springer, Berlin, 193-207. https://doi.org/10.1007/978-3-662-45231-8_14
Ballarini, P., Djafri, H., Duflot, M., Haddad, S. and Pekergin, N. (2011) Petri Nets Compositional Modeling and Verification of Flexible Manufacturing Systems. 2011 IEEE International Conference on Automation Science and Engineering, Trieste, 24-27 August 2011, 588-593. https://doi.org/10.1109/CASE.2011.6042488
[68]
Narahari, Y. and Viswanadham, N. (1994) Transient Analysis of Manufacturing Systems Performance. IEEE Transactions on Robotics and Automation, 10, 230-244. https://doi.org/10.1109/70.282547
[69]
Buzacoott, J.A. and Shantikumar, J.G. (1993) Stochastic Models of Manufacturing Systems. Prentice-Hall, New Jersey.
Mutarraf, U., Barkaoui, K., Li, Z.W., Wu, N. and Qu, T. (2018) Transformation of Business Process Model and Notation Models Onto Petri Nets and Their Analysis. Advances in Mechanical Engineering, 10, 168781401880817. https://hal.science/hal-02475788
[72]
van der Aalst, W.M.P. (1996) Three Good Reasons for Using a Petri-Net-Based Workflow Management System. In: Wakayama, T., Kannapan, S., Khoong, C.M., Navathe, S. and Yates, J., Eds., Information and Process Integration in Enterprises, Springer, Boston, 161-182.
[73]
van der Aalst, W.M.P. (1997) Verification of Workflow Nets. In: Azéma, P. and Balbo, G., Eds., ICATPN 1997: Application and Theory of Petri Nets 1997, Springer, Berlin, 407-426. https://doi.org/10.1007/3-540-63139-9_48
[74]
Meghzili, S., Chaoui, A., Strecker, M. and Kerkouche, E. (2016) Transformation and Validation of BPMN Models to Petri Nets Models Using GROOVE. 2016 International Conference on Advanced Aspects of Software Engineering (ICAASE), Constantine, 29-30 October 2016, 22-29. https://ieeexplore.ieee.org/abstract/document/7843859/authors
Barkaoui, K. and Petrucci, L. (1998) Structural Analysis of Workflow Nets with Shared Resources. In: van der Aalst, W.M.P., De Michelis, G. and Ellis, C.A., Eds., Workflow Management: Net-Based Concepts, Models, Techniques, and Tools (WFM’98): Proceedings of the Workshop, June 22, 1998, Lisbon, Portugal: WFM’98, Proceedings of the Workshop on Workflow Management. https://api.semanticscholar.org/CorpusID:60056523
[77]
Barkaoui, K., Boucheneb, H. and Hicheur, A. (2009) Modelling and Analysis of Time-Constrained Flexible Workflows with Time Recursive ECATNets. In: Bruni, R. and Wolf, K., Eds., WS-FM 2008: Web Services and Formal Methods, Springer, Berlin, 19-36. https://doi.org/10.1007/978-3-642-01364-5_2
[78]
Barkaoui, K. and Hicheur, A. (2012) Towards Analysis of Flexible and Collaborative Workflow Using Recursive ECATNets. In: ter Hofstede, A., Benatallah, B. and Paik, H.Y., Eds., BPM 2007: Business Process Management Workshops, Springer, Berlin, 232-244. https://doi.org/10.1007/978-3-540-78238-4_24
