تعميم مفهوم صحت ساختاري فرآیندهای کسب و کار از شبکه‌هاي پتري کلاسيک به مدل‌هاي فرآيندي BPMN
الموضوعات :
یحیی پورسلطانی
1
(فارغ التحصیل کارشناسی ارشد)
محمدحسن شیرعلی شهرضا
2
(دانشگاه صنعتی امیرکبیر)
سید علیرضا هاشمی گلپایگانی
3
(هیات علمی)
الکلمات المفتاحية: صحت ساختاری, زبان مدل‌سازی BPMN 2.0, شبکه‌هاي پتري, مدل‌هاي فرآيندي, کراندار بودن, زنده بودن,
ملخص المقالة :
استاندارد BPMN2.0 يک زبان مدل‌سازي به منظور طراحي فرآيندهاي کسب و کار مي‌باشد که به علت گويايي بالا، براي طيف وسيعي از کاربران قابل درک و استفاده مي‌باشد؛ با اين حال، به علت ماهيت غير صوري آن ممکن است مدل‌هايي حاوي خطاهايي ساختاري هم‌چون بن‌بست (عدم امکان اجرای فرآیند) و بن‌بست حلقوي (تکرار نامتناهی کارها) با استفاده از آن‌ها توليد شود. تاکنون تحقيقات زيادي پيرامون صحت‌سنجي اين مدل‌هاي فرآيندي صورت گرفته است و راهکارهاي مختلفي به منظور کشف برخی از این خطاهای ساختاری ارائه شده‌است؛ سوالی که در خصوص این روش‌ها ممکن است مطرح شود این است که آیا می‌توان با استفاده از هرکدام از آن‌ها صحت ساختاری یک مدل فرآیندی BPMN را به صورت قطعی تضمین کرد؟ برای پاسخگویی به این سوال نيازمند يک تعريف جامع از يک مدل فرآيندي BPMN2.0 صحيح هستيم تا بر مبنای آن بتوانیم جامعیت روش‌های صحت‌سنجی را مورد ارزیابی قرار داده و بدین وسیله، مطمئن شویم که روش ارائه شده می‌تواند تمامی خطاهای ساختاری مدل فرآیندی را کشف نماید. در اين پژوهش، بر پايه‌ي یک تعریف عام از مدل‌های فرآیندی و مفهوم صحت (بر اساس مدل‌هاي فرآيندي ايجاد شده با استفاده از شبکه‌هاي پتري) و تعميم ویژگی‌های آن، يعني زنده بودن و کراندار بودن به مدل‌هاي فرآيندي BPMN2.0، يک تعريف جامع براي یک مدل فرآيندي BPMN2.0 صحیح ارائه شده‌است و بر اساس آن، جامعیت روش‌های پیشنهادی برخی از مهم‌ترین پژوهش‌های صورت گرفته مورد ارزیابی قرار داده شده‌است؛ اين تعريف مي‌تواند به عنوان يک معيار براي سنجش کارايي روش‌هاي صحت‌سنجي اين مدل‌هاي فرآيندي به کار گرفته‌شود.
[1] Q. Nivon and G. Salaün, "Debugging of BPMN Processes Using Coloring Techniques," in Formal Aspects of Component Software, Cham, S. L. Tapia Tarifa and J. Proença, Eds., 2022// 2022: Springer International Publishing, pp. 90-109.
[2] F. Huang, F. Ni, J. Liu, F. Yang, and J. Zhu, "A Colored Petri Net Executable Modeling Approach for a Data Flow Well-Structured BPMN Process Model," IEEE Access, vol. 10, pp. 86696-86709, 2022, doi: 10.1109/ACCESS.2022.3198969.
[3] Y. Poursoltani, M. H. Shirali-Shahreza, and S. A. Hashemi Golpayegani, "Using Low-Code Development Platforms for developing Commercial Software based on Business Processes (wrote In Persian)," presented at the Conference: 26th International Computer Conference, Computer Society of Iran, Iran - Tehran, 1399 (In Persian). [Online]. Available: https://civilica.com/doc/1203571.
[4] R. Waszkowski, "Low-code platform for automating business processes in manufacturing," IFAC-PapersOnLine, vol. 52, no. 10, pp. 376-381, 2019/01/01/ 2019, doi: https://doi.org/10.1016/j.ifacol.2019.10.060.
[5] S. Braams, "Developing a Software Quality Framework for Low-Code Model Driven Development Platforms Based on Behaviour Driven Development Methodology.," presented at the 27th Twente Student Conference on IT, Enschede, The Netherlands., July 7th, 2017, 2017.
[6] O. M. Kherbouche, A. Ahmad, and H. Basson, "Detecting structural errors in BPMN process models," in 2012 15th International Multitopic Conference (INMIC), 2012: IEEE, pp. 425-431.
[7] O. M. Kherbouche, A. Ahmad, and H. Basson, "Using model checking to control the structural errors in BPMN models," IEEE 7th International Conference on Research Challenges in Information Science (RCIS), pp. 1-12, 2013.
[8] T. M. Prinz, N. Spieß, and W. Amme, "A First Step towards a Compiler for Business Processes," Berlin, Heidelberg, 2014: Springer Berlin Heidelberg, in Compiler Construction, pp. 238-243.
[9] M. Naoum, O. E. Hichami, M. A. Achhab, and B. E. E. Mohajir, "A probabilistic method for business process verification: Reachability, Liveness and deadlock detection," 2016 4th IEEE International Colloquium on Information Science and Technology (CiSt), pp. 128-132, 2016.
[10] F. Corradini, A. Morichetta, C. Muzi, B. Re, and F. Tiezzi, "Well-structuredness, safeness and soundness: A formal classification of BPMN collaborations," Journal of Logical and Algebraic Methods in Programming, vol. 119, p. 100630, 2021/02/01/ 2021, doi: https://doi.org/10.1016/j.jlamp.2020.100630.
[11] S. Meghzili, A. Chaoui, M. Strecker, and E. Kerkouche, "An Approach for the Transformation and Verification of BPMN Models to Colored Petri Nets Models," International Journal of Software Innovation (IJSI), vol. 8, no. 1, pp. 17-49, 2020, doi: 10.4018/IJSI.2020010102.
[12] M. Weske, "Business Process Modelling Foundation," in Business Process Management: Concepts, Languages, Architectures. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 73-124.
[13] R. M. Dijkman, M. Dumas, and C. Ouyang, "Semantics and analysis of business process models in BPMN," Information and Software Technology, vol. 50, no. 12, pp. 1281-1294, 2008/11/01/ 2008, doi: https://doi.org/10.1016/j.infsof.2008.02.006.
[14] C. Ou-Yang and Y. Lin, "BPMN-based business process model feasibility analysis: a petri net approach," International Journal of Production Research, vol. 46, no. 14, pp. 3763-3781, 2008.
[15] T. Takemura, "Formal Semantics and Verification of BPMN Transaction and Compensation," in 2008 IEEE Asia-Pacific Services Computing Conference, 9-12 Dec. 2008 2008, pp. 284-290, doi: 10.1109/APSCC.2008.208.
[16] K. Watahiki, F. Ishikawa, and K. Hiraishi, "Formal verification of business processes with temporal and resource constraints," in 2011 IEEE International Conference on Systems, Man, and Cybernetics, 9-12 Oct. 2011 2011, pp. 1173-1180, doi: 10.1109/ICSMC.2011.6083857.
[17] J. G. Peter Y.H. Wong, "Property specifications for workflow modelling," Science of Computer Programming, vol. 76, no. 10, pp. 942-967, 2011, doi: https://doi.org/10.1016/j.scico.2010.09.007.
[18] D. Falcioni, A. Polini, A. Polzonetti, and B. Re, "Livelock and Deadlock Detection for PA Inter-organizational Business Processes," in Advancing Democracy, Government and Governance, Berlin, Heidelberg, A. Kő, C. Leitner, H. Leitold, and A. Prosser, Eds., 2012// 2012: Springer Berlin Heidelberg, pp. 125-139.
[19] O. M. Kherbouche, A. Ahmad, and H. Basson, "Using model checking to control the structural errors in BPMN models," in IEEE 7th International Conference on Research Challenges in Information Science (RCIS), 29-31 May 2013 2013, pp. 1-12, doi: 10.1109/RCIS.2013.6577723.
[20] G. Barbon, V. Leroy, and G. Salaün, "Debugging of concurrent systems using counterexample analysis," in Fundamentals of Software Engineering: 7th International Conference, FSEN 2017, Tehran, Iran, April 26–28, 2017, Revised Selected Papers 7, 2017: Springer, pp. 20-34.
[21] O. El Hichami, M. Naoum, M. Al Achhab, I. Berrada, and B. E. El Mohajir, "An Algebraic Method for Analysing Control Flow of BPMN Models," International Journal of Recent Contributions from Engineering, Science & IT (iJES), vol. 3, no. 3, pp. pp. 20-26, 10/19 2015, doi: 10.3991/ijes.v3i3.4862.
[22] G. Decker, R. Dijkman, M. Dumas, and L. García-Bañuelos, "The Business Process Modeling Notation," in Modern Business Process Automation: YAWL and its Support Environment, A. H. M. Hofstede, W. M. P. Aalst, M. Adams, and N. Russell Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 347-368.
[23] W. v. d. A. a. K. v. H. The, Workflow Management. Models, Methods, and Systems. Massachusetts London,England: MIT Press Cambridge, 2002.
[24] R. Zurawski and M. Zhou, "Petri nets and industrial applications: A tutorial," IEEE Transactions on industrial electronics, vol. 41, no. 6, pp. 567-583, 1994.
[25] O. E. Hichami, M. Naoum, M. A. Achhab, I. Berrada, and B. E. E. Mohajir, "An Algebraic Method for Analysing Control Flow of BPMN Models," Int. J. Recent Contributions Eng. Sci. IT, vol. 3, no. 3, pp. 20-26, / 2015. [Online]. Available: https://www.online-journals.org/index.php/i-jes/article/view/4862.
[26] Y. Poursoltani, M. H. Shirali-Shahreza, and S. A. Hashemi Golpayegani, "Redefining the Soundness for BPMN2.0 Process Models, based on Petri nets," presented at the 5th National Conference on Advances in Enterprise Architecture (NCAEA), Mashhad- Iran, 2021. [Online]. (In Persian).Available: https://civilica.com/doc/1386000/.
Journal of Information and
Communication Technology
Volume 16, Issue 59-60, Spring and Summer 2024, pp. 195-213
Generalizing The Concept of Business Processes Structural Soundness from Classic Petri-nets to BPMN2.0 Process Models
Yahya Poursoltani1, Mohammad Hassan Shirali-Shahreza21, S.Alireza Hashemi Golpayegani3
1 Department of Mathematics and Computer Science, Amirkabir University of Technology, Tehran, Iran
2 Department of Mathematics and Computer Science, Amirkabir University of Technology, Tehran, Iran
3 APA Research Center-Information Technology Engineering Group, Amirkabir University of Technology, Tehran, Iran
Received: 18 February 2023, Revised: 02 April 2023, Accepted: 11 June 2023
Paper type: Research
Abstract
BPMN2.0 Standard is a modeling language, which can be understood and used by a wide range of users. However, because of its non-formal nature, models (designed using it) can be containing structural errors such as Deadlock (impossibility of executing some of process tasks) and Livelock (infinite repetition of tasks) may be produced by using them. These semantic errors can create anomalies in the workflow of the organization. So far, some researches has been conducted on the validation of these process models and various solutions have been provided to discover some of these structural errors. The question that may be raised about these methods is whether it is possible to definitely guarantee the structural accuracy of a BPMN method model by using any of them? To answer this question, we need a comprehensive definition of a correct BPMN2.0 process model, based on which we can evaluate the comprehensiveness of validation methods and strongly make sure that the considered method can discover all of the structural errors of the process model. In this paper, based on concept of general process models and the concept of soundness (based on process models created using Petri nets) and the generalization of its properties, i.e. Liveness and Boundness to BPMN2.0 process models, a comprehensive definition for a correct (sound) BPMN2 process model provided. Then, the comprehensiveness of the suggested methods of some of the most important researches conducted has been evaluated based on it. This definition can be used as a measure for efficiency of BPMN validation methods.
Keywords: Structural Soundness, BPMN2.0 Processes Models, Process Models, Liveness, Boundness.
تعميم مفهوم صحت ساختاري فرآیندهای کسب و کار از شبکه‌هاي پتري کلاسيک به مدل‌هاي فرآيندي BPMN
یحیی پورسلطانی1، محمد حسن شیرعلی شهرضا22، سید علیرضا هاشمی گلپایگانی3
1 دانش آموخته‌ی کارشناسی ارشد علوم کامپیوتر، دانشگاه صنعتی امیرکبیر(پلی تکنیک تهران)، تهران، ایران
2 استادیار، دانشکده ریاضی و علوم کامپیوتر، دانشگاه صنعتی امیرکبیر (پلی تکنیک تهران)، تهران، ایران
3 استادیار، مرکز پژوهشی آپا- گروه مهندسی فناوری اطلاعات، دانشگاه صنعتی امیرکبیر (پلی تکنیک تهران)، تهران، ایران
تاریخ دریافت: 29/11/1401 تاریخ بازبینی: 13/01/1402 تاریخ پذیرش: 21/03/1402
نوع مقاله: پژوهشی
چکيده
استاندارد BPMN2.0 يک زبان مدل‌سازي به منظور طراحي فرآيندهاي کسب و کار مي‌باشد که به علت گويايي بالا، براي طيف وسيعي از کاربران قابل درک و استفاده مي‌باشد؛ با اين حال، به علت ماهيت غير صوري آن ممکن است مدل‌هايي حاوي خطاهايي ساختاري هم‌چون بن‌بست (عدم امکان اجرای فرآیند) و بن‌بست حلقوي (تکرار نامتناهی کارها) با استفاده از آن‌ها توليد شود. تاکنون تحقيقات زيادي پيرامون صحت‌سنجي اين مدل‌هاي فرآيندي صورت گرفته است و راهکارهاي مختلفي به منظور کشف برخی از این خطاهای ساختاری ارائه شده‌است؛ سوالی که در خصوص این روش‌ها ممکن است مطرح شود این است که آیا می‌توان با استفاده از هرکدام از آن‌ها صحت ساختاری یک مدل فرآیندی BPMN را به صورت قطعی تضمین کرد؟ برای پاسخگویی به این سوال نيازمند يک تعريف جامع از يک مدل فرآيندي BPMN2.0 صحيح هستيم تا بر مبنای آن بتوانیم جامعیت روش‌های صحت‌سنجی را مورد ارزیابی قرار داده و بدین وسیله، مطمئن شویم که روش ارائه شده می‌تواند تمامی خطاهای ساختاری مدل فرآیندی را کشف نماید. در اين پژوهش، بر پايه‌ي یک تعریف عام از مدل‌های فرآیندی و مفهوم صحت (بر اساس مدل‌هاي فرآيندي ايجاد شده با استفاده از شبکه‌هاي پتري) و تعميم ویژگی‌های آن، يعني زنده بودن و کراندار بودن به مدل‌هاي فرآيندي BPMN2.0، يک تعريف جامع براي یک مدل فرآيندي BPMN2.0 صحیح ارائه شده‌است و بر اساس آن، جامعیت روش‌های پیشنهادی برخی از مهم‌ترین پژوهش‌های صورت گرفته مورد ارزیابی قرار داده شده‌است؛ اين تعريف مي‌تواند به عنوان يک معيار براي سنجش کارايي روش‌هاي صحت‌سنجي اين مدل‌هاي فرآيندي به کار گرفته‌شود.
کلیدواژگان: صحت ساختاری، زبان مدل‌سازی BPMN 2.0، شبکه‌هاي پتري، مدل‌هاي فرآيندي، کراندار بودن، زنده بودن.
[1] * Corresponding Author’s email: hshirali@aut.ac.ir
[2] * رایانامة نويسنده مسؤول: hshirali@aut.ac.ir
1- مقدمه
در طي دهه‌هاي اخير، با رشد فرآيندهاي تجاري و پيچيده‌تر شدن آن‌ها، لزوم ايجاد نرم‌افزارهايي براي مديريت آن‌ها روز به روز بيشتر حس مي‌شد [1]. پيچده‌تر شدن روزافزون فرآيندهاي کسب و کار منجر به افزايش شکاف بين تحليل‌گران، توسعه‌دهندگان نرم‌افزارها و کاربران نهايي شد[1]. به منظور کمک به کاهش این شکاف، استاندارد BPMN به منظور مدل‌سازي فرآيندهاي تجاري و توسط گروه مدیریت شی1 به وجود آمد و يکي از اهداف مهم آن، کاهش فاصله‌ي بين طراحان يک سيستم و توسعه‌دهندگان آن است؛ چرا که با استفاده از اين استاندارد مي‌توان فرآيندهاي کسب و کار را به صورتي بصري توصيف نمود[2]؛ در نتيجه توسط طیف وسیعی از کاربران (حتی کاربرانی که با دانش کامپیوتر آشنایی زیادی ندارند) قابل درک خواهد بود.
به گفته هانگ و همکاران [2] مدل‌های فرآیندی BPMN2.0 دارای دو ویژگی زیر هستند که منجر به ایجاد ماهیتي غیر صوری در آن می‌شود و در نتیجه، صحت‌سنجی و تحلیل آن را با دشواری‌هایی مواجه می‌سازد [2]:
1. زبان BPMN به عنوان یک زبان گراف‌گرای ایستا2 شناخته شده‌است.
2. شاخص مناسبی برای ارزیابی و پیش‌بینی رفتارهای پویای این مدل‌های فرآیندی (در زمان اجرا) وجود ندارد؛ این موضوع می‌تواند منجر به بروز خطاهایی در جریان کنترلی3 فرآیند و جریان اطلاعات4 در آن شود.
در نتیجه، نگاشت این مدل‌های فرآیندی به مدل‌هایی صوری می‌تواند به تحلیل بهتر آن‌ها کمک کند.
سادگي و گويايي این استاندارد، باعث شده‌است تا در بسياري از سکوهاي توسعه‌ی کم‌کد مثل Bizagi، Process Maker و يا سکوهاي ايرانيUbi Process و Bizotop، از آن به منظور ايجاد نرم‌افزارهاي سازماني، بدون نياز به کدنويسي و صرفا با ترسيم نمودارهاي BPMN، استفاده شود [3] [4]. در این خصوص، رابرت واتسکوزکی در قالب یک تحقیق، ضمن معرفی سکوهای توسعه‌ی کم کد و مبتنی بر زبان BPMN، اساسی‌ترین نیازمندی‌های کارکردی و غیرکارکردی این سکوها را تشریح کرد [4]. با استفاده از این سکوها، مدل‌های فرآیندی BPMN ترسیم می‌شوند؛ سپس بر مبنای مدل طراحی شده، بدون نیاز به برنامه‌نویسی، واسط‌های کاربری مورد نیاز برای اجرای فرآیندها ساخته می‌شود و نرم‌افزارهای اجراکننده‌ی آن مدل‌های فرآیندی، ایجاد شده و برای کاربران نهایی قابل استفاده می‌باشد [3, 4].
با فراگير شدن مدل‌هاي فرآيندي BPMN در بسياري از سکوهاي توسعه‌ي کم کد و ايجاد نرم‌افزار بدون نياز به دانش برنامه‌نويسي سنتي (نظير لزوم تسلط به زبان‌هاي برنامه‌نويسي متداول)، با کاربراني مواجه می‌شويم که به اين سکوها بيش از حد خوش‌بين هستند و ممکن است احساس کنند که با وجود اين سکوها و توليد نرم‌افزار با استفاده از آن‌ها، از بسياري از خطاهاي زمان اجرا جلوگيري مي‌شود؛ اين درحالي است که بروز خطاهاي ساختاري در مدل‌هاي فرآيندي BPMN و تبديل شدن آن به يک نرم‌افزار عملياتي مي‌تواند منجر به انتشار اين خطاها به سطوح مختلفي از نرم‌افزارهاي سازمان شود. در خصوص چالش تضمين کيفيت نرم‌افزارهاي ايجاد شده با استفاده از سکوهاي توسعه‌ي کم‌کد، استفان برامز[5] عدم وجود کدهاي کامپيوتري و درنتيجه، عدم امکان اجراي آزمون‌هاي متداول نرم‌افزاري نظير آزمون واحد5 را علتي بر بروز خطا در نرم‌افزارهاي ايجاد شده با استفاده از سکوهاي توسعه‌ي کم کد مي‌داند. با توجه به ماهيت غير صوري مدل‌هاي فرآيندي BPMN، طراحان فرآيند معمولا شاخص واضحي براي صحت‌سنجي مستقيم مدل‌هاي فرآيندي ندارند و ممکن است متوجه بروز بسياري از اين خطاهاي ساختاري نشوند. بنابراين اهميت صحت‌سنجي ساختاري مدل‌هاي فرآيندي BPMN پيش از اجراي عملياتي آن‌ها، بيش از پيش آشکار مي‌شود؛ چرا که ممکن است مدل‌هاي فرآيندي ايجاد شده به وسيله‌ي آن ناصحیح بوده و حاوي خطاهايي ساختاري نظير بن‌بست6 و يا بن‌بست حلقوي7 باشند؛ وجود اين خطاهاي ساختاري در اين مدل‌هاي فرآيندي، مي‌تواند ضمن ایجاد اختلال در گردش جریان کار سازمان، منجر به بروز اختلالاتي در سطوح مختلف معماري آن شود و يا ممکن است باعث ايجاد نرم‌افزاهايي با عملکردی ناصحیح شود.
در تحقيقات متعددي (از جمله [1]، [6]، [7]، [8]، [9] و [10])، راهکارهاي مختلفي به منظور صحت‌سنجي مدل‌هاي فرآيندي BPMN2.0 ارائه شده‌است؛ در هرکدام از آن‌ها، به کشف انواع مختلفی از خطاهاي ساختاري نظير بن‌بست‌ها، بن‌بست‌هاي حلقوي، پايان‌هاي چندگانه و غیره پرداخته شده‌است؛ بنابراين در هرکدام از آن‌ها، برداشت‌های مختلفی از یک مدل فرآیندی BPMN2.0 ناصحیح ارائه شده‌است و از شاخص واحد و مشخصی برای سنجش صحت یک مدل فرآیندی BPMN 2.0 صحیح استفاده نشده‌است؛ همچنین در بسیاری از این تحقیقات، شاخص‌های تاییدکننده‌ی صحت ساختاری مدل فرآیندی بر مبنای مدل‌های صوری (مدل صوری مقصد که مدل BPMN به آن تبدیل می‌شود) بیان شده‌اند؛ در نتیجه به صورت عینی برای کاربران نهایی و تحلیلگرانی که با آن مدل صوری آشنا نیستند، چندان قابل درک و ملموس نیستند [1]؛ حال آنکه بهتر است در ابتدا، این شاخص‌ها بر روی مدل مبدا (مدل BPMN) به صورتی ملموس و قابل مشاهده تعریف شده‌باشند و پس از صحت‌سنجی فرآیند در مدل مقصد، از برقرار بودن آن شاخص‌ها در مدل مبدا نیز اطمینان حاصل نمود؛ در صورتی که در خصوص یک نمونه مدل فرآیندی BPMN، تایید شاخص‌های صحت ساختاری در مدل مقصد منجر به تایید شاخص‌های صحت ساختاری مدل مبدا گردد، به معنای مناسب بودن و کارا بودن روش صحت‌سنجی می‌باشد. برای درک بهتر این ضرورت، به شکل 1 توجه کنید.
شکل 1. نمایی از جایگاه تعمیم مفهوم صحت ساختاری در مدل‌های فرآیندی BPMN
طبق شکل 1 مدل فرآیندی مبدا8 (یک مدل فرآیندی BPMN) حاوی عناصری می‌باشد که در قالب یک روش نگاشت 9، می‌تواند به یک مدل فرآیندی مقصد10 (مثل شبکه‌های پتری) نگاشته شود؛ در نتیجه در مدل مقصد یک بازنمایی جدید از آن مدل فرآیندی به وجود مي‌آيد. به منظور صحت‌سنجی ساختاری این مدل فرآیندی (در مدل مقصد) لازم است موارد زیر مشخص باشد:
1. شاخص‌هایی برای صحت مدل فرآیندی11 تعیین شده‌باشد تا بتوان بر مبنای آن‌ها، در خصوص صحیح بودن و یا صحیح نبودن مدل فرآیندی به صورت قطعی تصمیم گرفت.
2. الگوریتمی به منظور صحت‌سنجی مدل فرآیندی (بازنمایی شده در زبان مقصد) وجود داشته‌باشد که بر مبنای شاخص‌های صحت ساختاری (بند1)، صحیح بودن و یا صحیح نبودن مدل فرآیندی را تعیین نماید.
بدیهی است که اگر شاخص‌های صحت در مدل فرآیندی مقصد، شاخص‌های مناسبی نباشند آنگاه الگوریتم صحت‌سنجی ارائه شده در مدل فرآیندی مقصد نیز به درستی عمل نخواهد کرد؛ بنابراین برای آنکه از کارآمد بودن شاخص‌های صحت در مدل مقصد اطمینان حاصل نماییم، لازم است آن را با شاخص‌هایی کلی‌تر (که در زبان مدل‌سازی مبدا – یعنی زبان BPMN – قابل بیان باشد) مقایسه کرده و تطبیق دهیم و چنانچه این شاخص‌ها با یکدیگر معادل بودند، از کارآمدی شاخص‌های تعریف شده در مدل فرآیندی مقصد اطمینان حاصل می‌شود.
بنابراین در ابتدا لازم است یک تعریف کاملا مشخص و واحد، برای یک مدل فرآیندی BPMN2.0 صحيح (با بیان مدل مبدا) ارائه شود تا بتوان در ارزیابی کارهای انجام شده و نیز در تحقیقات بعدی بر اساس این تعریف، جامعیت و کارآمدی روش‌های صحت‌سنجی را ارزیابی نمود؛ علاوه بر آن يکي از موضوعات اساسي در انتقال مدل‌هاي نرم‌افزاري به يک ديگر، ارزيابي درستي انتقال مدل است که به معناي حصول اطمينان از معادل بودن مدل مقصد با مدل مبدا است؛ اين موضوع در حوزه‌ي مهندسي نرم‌افزار مدل رانده12، از اهميت بالايي برخوردار است [11]. بنابراين با دانستن مفهوم صحت ساختاري به بيان مدل‌هاي BPMN و انتقال اين مفاهيم به مدل مقصد، مي‌توان با مقايسه‌ي شاخص‌هاي صحت در مدل مقصد با انتقال يافته‌ي شاخص‌هاي صحت مدل‌هاي BPMN، از مناسب بودن شاخص‌هاي صحت در مدل مقصد اطمينان حاصل نمود.
در اين پژوهش، با در نظر گرفتن مدل‌هاي فرآيندي BPMN2.0 به عنوان يک مدل فرآيندي (بر اساس مفهوم عام و کلی یک مدل فرآیندی-پیشنهاد شده توسط ماتیاس وسکی و همکارانش [12])، بر مبناي يک نگاشت بين شبکه‌هاي پتري و مدل‌هاي فرآيندي BPMN2.0 (پیشنهاد شده توسط داکمن و همکارانش [13])، دو مشخصه‌ي يک مدل فرآیندی صحیح ایجاد شده به وسیله‌ی شبکه‌های پتری، يعني زنده بودن13 و کراندار بودن14، به مدل‌هاي فرآيندي BPMN2.0 تعميم داده شده‌اند و در نهايت، مفهوم صحت از شبکه‌هاي پتري به صحت مدل‌هاي فرآيندي BPMN2.0 تعميم داده شده‌است (مسیر فلش خط‌چین قرمزرنگ در شکل 1). بنابراین در این تحقیق به این سوالات پاسخ داده شده‌است:
1. تصدیق صحت یک مدل فرآیندی BPMN (با بیان زبان مدل‌سازی BPMN) بر مبنای چه ویژگی‌هایی باید صورت گیرد؟
2. ویژگی‌های بدست آمده برای صحت یک مدل فرآیندی BPMN (با بیان زبان مدل‌سازی BPMN) در چه وضعیتی باشند تا بتوان گفت که آن مدل فرآیندی صحیح است؟
3. این ویژگی‌ها به چه شکلی در مدل فرآیندی مبدا (به زبان BPMN) خود را نشان می‌دهند؟
4. روش‌های پیشنهاد شده در تحقيقات پيشين به منظور صحت‌سنجی مدل‌های فرآیندی BPMN (در مدل‌های مقصد و بازنمایی شده با مدل‌های صوری) تا چه حدی این ویژگی‌ها و مفهوم تعمیم یافته‌ی صحت را ارضا مي‌کنند و با آن مطابقت دارند؟
این مقاله در 4 بخش اساسی مقدمه، روش پیشنهادی، یافته‌های پژوهش و نتیجه‌گیری سازماندهی شده‌است. در بخش مقدمه، پس از بیان ضرورت و کلیاتی از موضوع پژوهش (بخش کنونی)، به بررسی پیشینه‌ی پژوهش (مرور کارهاي قبلي) و اساسی‌ترین مفاهیم مورد نیاز برای پیشبرد آن پرداخته شده‌است. سپس در بخش دوم (روش پیشنهادی)، به بیان شاخص‌های پیشنهادی برای صحت یک مدل فرآیندی BPMN (در مدل مبدا) می‌پردازیم و در قالب سه گام اساسی، درست بودن این شاخص‌ها را بر مبنای شبکه‌های پتری اثبات می‌کنیم. در بخش سوم (یافته‌های پژوهش)، خطاهای ساختاری را که توسط کارهای مطرح شده در بخش مقدمه (و زيربخش پيشينه‌ي پژوهش) پوشش داده شده‌اند، با ویژگی‌ها و تعاریف پیشنهادی خود تطبیق داده و در خصوص کارایی آن‌ها بحث می‌کنیم و با یک نتیجه‌گیری، این پژوهش به اتمام می‌رسد.
1-1- پيشينه‌ي پژوهش
در خصوص صحت‌سنجي مدل‌هاي فرآيندي BPMN2.0، از روش‌های مختلفی استفاده شده‌است که در هرکدام از آن‌ها، به کشف انواع مختلفي از خطاهاي ساختاري پرداخته شده‌است. در بسياري از تحقيقات صورت گرفته، کشف بن‌بست‌ها، جزو اهداف اصلي صحت‌سنجي ساختاری این مدل‌های فرآیندی بوده‌است. در این بخش قصد داریم مروری بر تحقیقات صورت گرفته درخصوص روش‌های صحت‌سنجی ساختاری مدل‌های فرآیندی BPMN و خطاهای ساختاری پوشش داده شده توسط هرکدام از آن‌ها بپردازیم.
اولین تحقیقات حوزه‌ي صحت‌سنجي مدل‌هاي فرآيندي BPMN توسط داکمن و همکارانش در سال 2008 صورت گرفت [13]؛ در این تحقیق، یک روش برای نگاشت مدل‌های BPMN به شبکه‌های پتری به منظور شناسایی خطای ساختاری بن‌بست ارائه شد [13]. به دنبال انجام اين تحقيق و مطرح شدن شبکه‌هاي پتري کلاسيک به عنوان يکي از کارآمدترين مدل‌هاي صوري براي صحت‌سنجي ساختاري مدل‌هاي فرآيندي BPMN، استفاده از آن در تحقیقات بعدی ادامه یافت؛ از جمله می‌توان به تحقیق او-يانگ و همکارش در همان سال اشاره نمود[14]. در اين تحقيق به بررسي دسترسي‌پذيري15، کشف بن‌بست و نيز کشف بن‌بست حلقوی با استفاده از شبکه‌هاي پتري پرداخته شده‌است؛ در همان سال تاکمورا و همکارانش به ارائه‌ي يک روش مبتني بر شبکه‌هاي پتري به منظور صحت‌سنجي تراکنش‌هاي مدل‌سازي شده به وسيله‌ي مدل‌هاي فرآيندي BPMN پرداختند[15] ؛ با اين کار، به صحت‌سنجی بخش‌هایی از فرآیند که امکان لغو تراکنش در آن وجود داشت، پرداخته شده‌است [15]؛ چرا که در بسياري از مواقع لغو تراکنش مي‌تواند منجر به بروز بن‌بست و يا بن‌بست حلقوي شود.
در سال 2011 تحقیقی توسط واتاهیکی و همکاران انجام شد که در آن، روشی برای صوری‌سازی مدل‌های BPMN ارائه شد که از آن به منظور جلوگیری از بروز خطاهای معنایی در فرآیندهایی که در منابع و زمان دچار محدودیت هستند، استفاده شد [16]. در این پژوهش، مدل فرآیندی BPMN گسترش داده شده و سپس به یک اوتوماتای زمانی نگاشته شده‌است؛ سپس اوتوماتای زمانی بدست آمده، با ابزاری به نام UPPAL مورد ارزیابی قرار گرفته‌است[16]. هدف از اجراي اين پژوهش، کشف نقاط گلوگاهي و بن‌بست در مدل‌هاي فرآيندي BPMN و داراي منابع محدود بود؛ در همان سال استفاده از ساير روش‌هاي صوري نيز مورد توجه قرار گرفت و در نتيجه، روشي توسط وانگ و همکارانش پيشنهاد شد[17]. در اين روش، از منطق زماني خطي (يا منطق زماني موقت16) به منظور پيش‌بيني خطاهاي بن‌بست و بن‌بست حلقوي استفاده شده‌است.
يکي از موقعيت‌هايي که ممکن است منجر به ايجاد خطاهاي ساختاري در مدل‌هاي فرآيندي شود، جريان يافتن فرآيند در بين چند سازمان است؛ در چنين حالتي، جريانی از تعاملات در بين سازمان‌ها ايجاد شده و فرآيندهاي هرکدام از آن‌ها، به صورتي غيربديهي مي‌تواند با فرآيند ديگری ادغام گردد. برای کشف خطاهای احتمالی و ناشی از تعاملات بین سازمانی، در سال 2012 تحقیقی توسط فالسيوني و همکاران صورت گرفت [18] ؛ آن‌ها با به کارگيري يک الگوريتم بخش‌بندی17، توانستند راهکاري را به منظور بررسي وجود اثرات مخرب بر روي فرآيندهای تعاملی18 بین سازمانی و در نتيجه، کشف بن‌بست و بن‌بست حلقوي ارائه کنند [18].
در بین روش‌های صحت‌سنجي مدل‌های BPMN، روش‌های مبتنی بر وارسی مدل19 نیز در صحت‌سنجی ساختاری مدل‌های فرآیندی BPMN مورد توجه بوده‌است؛ به عنوان نمونه می‌توان به تحقیقات صورت گرفته توسط خربوشه و همکاران وی در سال‌هاي 2012 و 2013 اشاره نمود [6, 7]؛ در این تحقیقات، مدل فرآیندی BPMN به ساختاری به نام ساختار کریپکی20 نگاشته شد و سپس، از منطق زمانی خطی (يا منطق زماني موقت21) به منظور صحت‌سنجی ساختاری مدل فرآیندی (به منظور اطمينان از عدم وجود بن‌بست، بن‌بست حلقوی و پایان‌های چندگانه) استفاده شده‌است [19]. این روش دارای زمان اجرای مناسب بوده و با استفاده از آن امکان تعقیب مسیر حاوی خطا، وجود دارد. در سال 2014 در طی پژوهش صورت گرفته توسط پرینز و همکاران [8] یک زبان میانی برای بازنمایی صوری مدل‌های BPMN معرفی شد. این زبان میانی به گراف جریان22 کار موسوم شد و به منظور ایجاد یک کامپایلر برای مدل‌های BPMN مورد استفاده قرار گرفت و بر روی نرم‌افزار Eclipse مستقر شد؛ اگرچه مدل میانی پیشنهاد شده، ساده و قابل فهم است، اما این روش دارای محدودیت بوده و از مدل‌های فرآیندی پیچده با عناصر متعدد پشتیبانی نمی‌کند[8]. توسعه‌ی روش‌های مبتنی بر وارسی مدل تا سال‌های اخیر (سال 2023) نیز از محبوبیت زیادی برخوردار بوده‌است؛ در این خصوص می‌توان به تحقیق صورت گرفته توسط نیون و همکارانش اشاره نمود که در سال 2022 صورت گرفت [1]؛ روش مورد استفاده در این کار، بر مبنای وارسی مدل23 است و توسط یک وارسی‌گر مدل24 مورد بررسی قرار می‌گیرد. مدل فرآیندی داده شده، توسط وارسی‌گر مدل بررسی می‌شود و اگر ویژگی‌های مورد نظر (صحیح بودن) را ارضا نماید، وارسی گر یک نتیجه‌ی TRUE تحویل میدهد و در غیر این صورت، یک مثال نقض که منجر به نقض ویژگی مورد نظر می‌شود، توسط آن تولید می‌شود. مثال نقض ایجاد شده، بر مبنای یک مدل صوری به نام LTS 25 بیان شده‌است که درک آن توسط کاربران عادی ممکن است دشوار باشد؛ چرا که این زبان، یک زبان رسمی برای توصیف مدل است که علاوه بر توصیف مدل‌های BPMN، در توصیف سیستم‌های هم روند نیز مورد استفاده قرار می‌گیرد [20]؛ برای درک بهتر مثال‌های نقض توسط کاربران نهایی، در این کار یک روش رنگ آمیزی پیشنهاد شده‌است که مثال نقض ایجاد شده را (که به وسیله‌ی LTS توصیف گشته‌است) به یک مدل BPMN تبدیل کرده و به صورتی واضح (رنگ آمیزی شده) در اختیار کاربر نهایی قرار مي‌دهد.
به گفته‌ی صریح نویسندگان مقاله‌ی[1]، عمده‌ی هدف آن معطوف بر تصدیق ویژگی زنده بودن (قابل اجرا بودن تمامی فعالیت‌های فرآیند) در مدل‌های فرآیندی BPMN است. با این حال، در این مقاله به مفهوم امن بودن مدل فرآیندی نیز توجه شده‌است [1].
در بین روش‌های صحت‌سنجي، روش‌های مبتني بر جبر رياضي نیز مورد استقبال بودند؛ از جمله‌ی روش‌های مدل‌سازی ریاضی می‌توان به بیان صوری مدل‌های BPMN در زبان جبر ماکس پلاس26 و سپس صحت‌سنجي آن اشاره نمود که توسط الحکمی در سال 2015 ارائه شد [21]؛ در اين کار، از عدم امکان وقوع بن‌بست و وقوع پايان‌هاي چندگانه اطمينان حاصل مي‌گردد.
یکی از دغدغه‌های اصلی کارهای قبلی، پیچیده بودن فرآیند تبدیل و انتقال مدل‌های BPMN به مدل مقصد بود؛ برای رفع این مشکل، در سال 2016، نوم و همکاران یک روش مبتنی بر تحلیل احتمالاتی اجزای BPMN به منظور صحت‌سنجی ساختاری آن ارائه کردند[9]؛ در اين پژوهش، بر مبناي قاعده‌ي ضرب احتمالات27، احتمال وقوع بن‌بست در مدل فرآيندي قابل محاسبه است.
در سال 2021 تحقیقی توسط فلاویو کوردینی و همکارانش در این خصوص صورت گرفت. تحقیق ایشان عمدتا دربرگیرنده‌ی مدل‌های فرآیندی تعاملی28 است[10]. همان‌طور که می‌دانیم مدل‌های فرآیندی BPMN می‌توانند حاوی بیش از یک Pool باشند که هرکدام از آن‌ها، در برگیرنده‌ی فرآیندهای یک سازمان هستند. این بخش‌ها می‌توانند با یکدیگر تعامل کنند و در نتیجه، تعامل بین سازمان‌ها نیز مدل‌سازی می‌شود. این تعامل (همان‌طور که در تحقیق فالسیونی و همکاران [18] به آن اشاره شده‌است) می‌تواند به صورتی غیر مستقیم منجر به ایجاد خطاهای ساختاری شود. در این تحقیق یک روش صوری به منظور ارزیابی برقراری سه شاخص مرتبط با صحت ساختاری، به منظور صحت‌سنجی مدل‌های فرآیندی BPMN تعاملی ارائه شده‌است [10]. این سه شاخص عبارتند از صحت29، امنیت30 و خوش‌ساختاری31 ؛ شاخص صحت متضمن اجرا شدن تمام فعالیت‌ها و امنیت متضمن عدم تکرار نامتناهی فعالیت‌ها می‌باشد. در کنار این دو ویژگی، خوش‌ساختار بودن نیز به عنوان یک ویژگی معرفی شده‌است که به معنای جمع شدن شاخه‌های انشعابی توسط یک دروازه اتصالی است. در بخشی از این کار تحقیقاتی، ارتباط بین این سه ویژگی به صورت دو به دو بررسي شد و در پایان آن، فرآیندهای کسب و کار از نظر قابليت ارضای این سه ویژگی دسته‌بندی می‌شوند [10]. در پایان این مقاله، یک ابزار به منظور صحت‌سنجی مدل‌های فرآیندی BPMN و بر اساس روش صوری پیشنهاد شده، ایجاد گشته و بر روی تعدادی از مدل‌های فرآیندی BPMN و تعاملی اجرا شد. اما در پایان و در نتایج این مقاله، مشخص شده‌است که صحیح نبودن یک فرآیند، لزوما امن بودن آن را نقض نمی‌کند؛ اما در صورتی که یک مدل فرآیندی خوش‌ساختار باشد، الزاما صحیح و امن است [10]. لازم به ذکر است که شاخص صحيح بودن در مقاله‌ي کورديني با شاخص صحيح بودن در اين پژوهش، تفاوت‌هايي دارد و خاص منظوره تر است.
همان‌طور که ديده شد، در تحقيقات مختلف، روش‌هاي مختلفي براي کشف اين خطاي ساختاري صورت گرفته‌است و در بين تمام خطاهاي ساختاري، کشف بن‌بست از اهميت زیادی برخوردار بود و در وهله‌ي بعدي، کشف بن‌بست حلقوي جزو اهداف برخي از اين تحقيقات، از جمله [1]، [6]، [7]، [8]، [9] و [10] بوده‌است. همچنين در برخی ديگر از تحقیقات، به بررسی وجود انواع دیگری از خطاها پرداخته شده‌است؛ به عنوان مثال، در پژوهش [16] به کشف نقاط گلوگاهی در مدل‌های فرآیندی و در پژوهش [14] به کشف حلقه‌های نامتناهی پرداخته شده‌است. همچنین در برخی از پژوهش‌ها مثل [6]، [7] و [9]، وجود حالات پایانی متعدد نیز به عنوان خطاهایی ساختاری در نظر گرفته شده‌است.
همان‌طور که مشاهده شد، در تمامي تحقیقات صورت گرفته، صحت‌سنجی بر مبنای فهرست معيني از خطاهاي ساختاري صورت گرفته‌است؛ بنابراين بر مبناي یک تعریف جامع از یک مدل فرآيندي صحیح صورت نگرفته‌است؛ در نتيجه در هرکدام از آن‌ها، ممکن است فقط بخشی از جنبه‌های صحت یک مدل فرآیندی بررسی شده‌باشد و بخشي از جنبه‌هاي صحت آن، بررسي نگردد؛ به عنوان مثال ممکن است در يکي از روش‌هاي صحت‌سنجي، در يک مدل فرآيندي BPMN ورودي امکان وقوع بن‌بست کشف شود، اما امکان وقوع بن‌بست حلقوي کشف نشود (درحالي که امکان وقوع بن‌بست حلقوي در آن مدل فرآيندي وجود داشته‌باشد). در نتيجه لازم است که یک تعریف جامع برای یک مدل فرآیندی BPMN صحیح ارائه شود تا جامعيت روش‌های صحت‌سنجی بر مبناي آن سنجيده شود؛ علاوه بر این، همانند تحقیق صورت گرفته توسط نیون و همکاران [1]، این تعاریف به انتقال بهتر ویژگی‌های صحت ساختاری به کاربر نهایی نیز کمک می‌کند و او را از لزوم درک ویژگي‌هاي صحت ساختاري در قالب مدل‌هاي صوري معاف مي‌کند؛ چرا که تعاریف پیشنهادی در قالب زبان BPMN بیان می‌شود و در نتیجه صحت ساختاری یک مدل فرآیندی BPMN، بر روی خود مدل قابل درک و بررسی خواهد بود؛ از سوي ديگر، در روش‌هاي مبتني بر مهندسي نرم‌افزار مدل رانده، لازم است از درستي روش نگاشت بين مدل‌ها اطمينان حاصل نمود؛ در اين رويکرد، نگاشتي درست است که در آن، مدل‌هاي مبدا و مقصد با يک ديگر هم‌ارز باشند. به عنوان مثال در اين خصوص، تحقيقي توسط مغزيلي و همکارانش در سال 2020 صورت گرفت که در آن، روشي به منظور اطمينان از درستي نگاشت مدل‌هاي فرآيندي BPMN به شبکه‌هاي پتري رنگي ارائه شد [11]؛ با توجه به ضرورت صحت‌سنجي نگاشت‌هاي پيشنهادي، لازم است براي اطمينان از صحيح بودن شاخص‌هاي صحت ساختاري در يک مدل صوري (به عنوان مدل مقصد)، شاخص‌هاي صحت در مدل مبدا، مشخص بوده و پس از نگاشت به مدل مقصد، با شاخص‌هاي صحت ساختاري مدل مقصد مقايسه شود تا بدين وسيله، از مناسب بودن نگاشت پيشنهادي اطمينان حاصل شود.
در این پژوهش، مفهوم صحت ساختاري را در مدل‌های فرآیندی BPMN2.0 بر اساس صحت شبکه‌ی پتری معادلشان بازتعریف می‌کنیم. این کار را با تعمیم مفاهیم زنده بودن و کراندار بودن از شبکه‌های پتری به مدل‌هاي فرآيندي BPMN2.0 انجام خواهيم داد.
1-2- مفاهیم اساسی مورد نیاز
هر پژوهش بر مبناي بنيان‌هاي نظري توسعه داده شده توسط پژوهش‌هاي پيشين رشد مي‌کند و اين تحقيق نيز از اين قاعده مسثني نيست؛ بنابراين در اين بخش، به بيان بنيان‌ها و نتايجي از تحقيقات پيشين مي‌پردازيم که در پژوهش جاري مورد استفاده قرار گرفته‌است.
1-2-1- مفهوم مدل‌هاي فرآيندي (به صورت عام)
مدل‌های فرآیندی BPMN2.0، شبکه‌های پتری و دیگر زبان‌های مدل‌سازی فرآیندها، دارای یک خصیصه‌ی مشترک هستند: «همه‌ی آن‌ها، یک فرآیند کاری را توصيف می‌کنند»؛ بنابراین، همگی آن‌ها مدل‌هایی فرآیندی32 هستند. بنابراین نتیجه می‌گیریم که هر مدل فرآیندی، با زبان‌های مختلفی می‌تواند توصيف شود (مشابه با زبان گفتاري که در آن يک مفهوم واحد مي‌تواند به زبان‌ها و گويش‌هاي مختلفي گفته شود) و این مفهوم، مستقل از زبان مدل‌سازی می‌باشد. به همین منظور، ماتیاس در کتاب مدیریت فرآیندهای کسب و کار، با در نظر گرفتن مدل فرآيندي به عنوان يک مفهوم عامي که در زبان‌هاي مختلفي قابل بيان است، یک تعریف مشخص و جامع را ارائه کرده‌است [12]:
تعريف 1 (مدل‌های فرآیندی) یک مدل فرآیندی، یک گراف جهت‌دار است مثل 
به طوری‌که 
مجموعه‌ی یال‌های آن و 
مجموعه‌ی گره‌های آن است که به سه زیرمجموعه افراز می‌شوند:
1. مجموعه‌ی مدل‌های فعالیتی33 که هرکدام از اعضای آن نشان‌دهنده‌ی یک فعالیت در مدل فرآیندی هستند. این زیرمجموعه با 
نشان داده می‌شود.
2. مجموعه‌ی مدل‌های رخدادی34 که هرکدام از اعضای آن نشان‌دهنده‌ی یک رخداد در مدل فرآیندی هستند. این مجموعه با 
نشان داده می‌شود.
3. مجموعه‌ی مدل‌های دروازه‌ای35 که هرکدام از اعضای آن نشان‌دهنده‌ی یک دروازه (انشعابی و یا اتصالی) در مدل فرآیندی می‌باشند. این مجموعه با 
نشان داده می‌شود.
بنابراین، هر فرآیند مدل‌سازي شده با BPMN را مي‌توان يک مدل فرآیندی دانست که در آن، مجموعه‌ی مدل‌های فعالیتی، رخدادی و دروازه‌ای متناظر است با فعالیت‌ها، رخدادها و دروازه‌ها در مدل فرآیندی BPMN2.0. بنابراین، یک مدل فرآیندی BPMN2.0 مثل 
می‌تواند به صورت 
تعریف شود به طوری که مجموعه‌ي به سه زيرمجموعه‌ي فعاليت‌ها ()، رخدادها () و دروازه‌ها () افراز شود. بنابراین خواهیم داشت:
به گونه‌ای که:
1-2-2- شبکه‌هاي جريان کار
براي تعميم مفهوم صحت به مدل‌هاي فرآيندي BPMN2.0، لازم است این مدل فرآیندی يک شبکه‌ي جريان کاري36 باشد [17]. يک شبکه‌ي جريان کار، فرآيندي است که داراي دقیقا يک نقطه‌ي شروع و دقیقا يک نقطه‌ي پاياني باشد [17]. بايد توجه کرد که در صورتي که يک فرآيند داراي ويژگي يک شبکه‌ي جريان کار نباشد، مي‌تواند با اعمال تغييراتي به يک شبکه‌ي جريان کار تبديل شود:
1. تمامي شاخه‌هاي منتهي به رخدادهاي پاياني، به يک دروازه‌ي انحصاري متصل شود (از نوع اتصالي) و خروجي دروازه، به يک رخداد پاياني متصل شود.
2. تمامي شاخه‌هاي آغاز شده از رخدادهاي شروع، به واسطه‌ي يک دروازه‌ي انحصاري (انشعابي) به يک رخداد شروع یکتا متصل شود.
با اين کارها، فرآيند داده شده به يک شبکه‌ي جريان کار تبديل خواهد شد. چرا که فرآيند، دقيقا با يکي از رخدادهاي آغازين، شروع شده و دقيقا با يکي از رخدادهاي پاياني، پايان مي‌يابد. بنابراين، مفهوم تعميم يافته‌ي صحت، مي‌تواند براي تمامي انواع مختلفي از مدل‌هاي فرآيندي BPMN2.0 به کار رود.
اگرچه در برخي از کارهاي پژوهشي مثل [6]، [7] و [9] وجود پايان‌هاي چندگانه به عنوان خطاهاي ساختاري در نظر گرفته شده‌است، اما در استاندارد BPMN وجود شروع‌هاي چندگانه (مشروط بر آنکه بجز يک رخداد شروع، ساير رخدادهاي آغازين به صورت شروع با تحريک37 باشند) و پايان‌هاي چندگانه مجاز است [22] و چنين ويژگي منجر به نقض صحت ساختاري مدل‌هاي فرآيندي (توصیف شده با استاندارد BPMN) نمي‌شود.
1-2-3- مفهوم صحت (بر اساس شبکه‌هاي پتري)
بر طبق تعریف ارائه شده توسط آلست و همکارانش[23] یک فرآیند ایجاد شده با استفاده از شبکه‌ی پتری صحیح38 است، اگر و تنها اگر دو ویژگی زیر در خصوص آن برقرار باشد:
1. فرآیند، زنده39 باشد.
2. فرآیند، کراندار40 باشد.
زوراسکی، در مقاله‌ی آموزشی خود در خصوص شبکه‌های پتری، ویژگی زنده بودن را بدین صورت تعریف می‌کند[24]:
تعريف 2 (زنده بودن یک شبکه‌ی پتری): «یک شبکه‌ی پتری زنده‌است، اگر و تنها اگر هر نشانه‌گذاری مثل به بیان ساده‌تر، در [23] زنده بودن بدین صورت تعریف شده‌است: تعريف 3 « یک شبکه‌ی پتری زنده است، اگر و تنها اگر تمامی انتقال‌های آن، در موقعیتی بتوانند فعال شده و شلیک شوند.» ویژگی زنده بودن برای یک فرآیند، تضمین می‌کند که تمامی فعالیت‌های آن، اجرا می‌شوند و در نتيجه وجود خطاهايي ساختاري مثل بن‌بست41، کارهاي مرده42 و فعاليت‌هاي بدون ورودي و يا خروجي، منتفي است. يکي ديگر از ويژگي‌هايي که براي صحيح بودن يک فرآيند لازم است، کراندار بودن است؛ زوراسکی در مقاله‌ی آموزشی خود در خصوص شبکه‌های پتری[24] این ویژگی را به صورت زیر تعریف می‌کند: تعريف 4 (کراندار بودن یک شبکه‌ی پتری): «یک شبکه‌ی پتری را اين ویژگی بيان مي‌کند که برای یک شبکه‌ی پتری مثل 1-2-4- نگاشت بين مدل‌هاي فرآيندي BPMN2.0 و شبکه‌هاي پتري در اين پژوهش، نگاشت ارائه شده توسط داکمن و همکارانش[13] مبنایی برای صوري‌سازي مدل‌هاي فرآيندي BPMN2.0 و تعميم مفهوم صحت از شبکه‌های پتری به مدل‌های BPMN قرار گرفته‌است. در این نگاشت (در جدول 1 نشان داده شده‌است) هرکدام از ساختارهاي مدل‌هاي فرآيندي BPMN2.0 به يک ساختاري از شبکه‌هاي پتري نگاشته شده‌است. جدول 1. نگاشت ارائه شده توسط داکمن در [13] نوع گره (یا ساختار) از منظر مدل‌های فرآیندی عام عنصر در زبان BPMN معادل عنصر در شبکه‌های پتری فعالیتی رخدادی دروازه‌ای همان‌طور که در جدول 1 مشاهده مي‌شود، انتقال‌هايي که درجه‌ي ورودي و يا خروجي بزرگ‌تر از 1 دارند، معادل با دروازههای موازی هستند و انتقال‌هايي که درجه‌ي ورودي و خروجي برابر با 1 است، معادل با رخدادها و یا فعاليت‌ها هستند. با تکیه بر این واقعیت که تعریف 1 در خصوص مدل‌های فرآیندی ایجاد شده با استفاده از استاندارد BPMN و شبکه‌های پتری صادق است (چون هردو نشان‌دهنده‌ی یک مدل فرآیندی هستند) می‌توان اجزای BPMN و اجزای معادل آن‌ها را به سه مجموعه‌ی مدل‌های فعالیتی، رخدادی و دروازه‌ای تقسیم نمود. البته در خصوص شبکه‌های پتری لازم است کارکرد انتقال از قبل مشخص باشد. این تقسیم بندی در ستون نوع گره (یا ساختار) بر مبنای مدل‌های فرآیندی عام (تعریف 1) گفته شده‌است. 1-2-5- نقض زنده بودن فرآيند به علت وقوع بن‌بست آلست ون هی و همکارانش [23] در کتاب مدیریت جریان‌های کاری، برای یک شبکه‌ی پتری مثل تعريف 7 (بن‌بست): «بن‌بست به وضعیتی اطلاق می‌شود که در طی آن، توکن متناظر با یکی از موارد کاری در یکی از مکان‌ها باقی بماند و هیچ کدام از انتقال‌های پس از آن شلیک نشوند؛ در نتیجه امکان خروج توکن از آن مکان به هیچ وجه میسر نخواهد بود.» به عنوان نمونه، در شکل 2 یک نمونه از بروز بن‌بست در یک مدل فرآیندی BPMN2.0 قابل مشاهده است. شکل 2. نمونه‌اي از بروز خطاي ساختاري بن‌بست در این شکل با شروع فرآیند و رسیدن جریان فرآیند به دروازه‌ی انحصاری، دقیقا یکی از شاخه‌های دروازه‌ی انحصاری را فعال می‌کند؛ در نتیجه، جریان فرآیند از یکی از خروجی‌های دروازه‌ی انحصاری ادامه یافته و فقط یکی از ورودی‌های دروازه‌ی موازی (هم‌گام سازی) فعال خواهد شد؛ این درحالی است که ادامه‌ی اجرای فرآیند منوط به فعال شدن تمامی ورودی‌های دروازه‌ی هم‌گام سازی (دروازه‌ی موازی اتصالی) است؛ در نتیجه، در محل این دروازه، یک بن‌بست رخ خواهد داد. حال، این مدل فرآیندی را بر طبق جدول 1 به یک شبکه‌ی پتری نگاشت می‌دهیم. در نتیجه شکل 3 بدست می‌آید. شکل 3. تبديل يافته‌ي مدل فرآيندي ترسيم شده در شکل 2 به شبکه‌ي پتري معادل بر اساس نگاشت داکمن در شکل 3 در صورتی که یک توکن از مکان شروع (مکان 1-2-6- بن‌بست حلقوي تکرار فعالیت‌های یک فرآیند به صورت نامتناهی، یکی از مشکلاتی است که صحت ساختاری آن را تهدید می‌کند. مدل فرآیندی ترسیم شده در شکل 4 مثالی از وقوع این مشکل در یک مدل فرآیندی BPMN می‌باشد. شکل 4. نمونه‌ای از بروز بن‌بست حلقوی در یک مدل فرآیندی BPMN2.0 در شکل 4 بعد از اجرای فعالیت Task1، دو فعالیت بعدی اجرا می‌شوند. سپس، جریان اجرای فرآیند به یک دروازه‌ی موازی می‌رسد. با موازی‌سازی جریان فرآیند، فرآیند از هر دو مسیر خروجی آن ادامه می‌یابد و در نتیجه، دو فعالیت Task1 و Task2 اجرا می‌شوند؛ سپس یکی از این شاخه‌ها به نقطه‌ی پایان رسیده و ظاهرا فرآیند به اتمام می‌رسد؛ این درحالی است که چنین اتفاقی رخ نمی‌دهد و در حالی که اجرای یکی از شاخه‌ها به پایان رسیده است، شاخه‌ی دیگر خروجی دروازه‌ی موازی، جریان فرآیند را به ورودی دروازه‌ی انحصاری هدایت می‌کند و مجددا هر دو فعالیت‌های Task2 و Task3 اجرا می‌شوند و این روند ادامه می‌یابد؛ در نتیجه، دو فعالیت Task2 و Task3 به تعداد دفعات نامتناهی اجرا می‌شوند و یک حلقه‌ی اجرایی نامتناهی در فرآیند اجرا می‌شود. در چنین شرایطی در محل دروازه‌ی انشعاب موازی، یک بن‌بست حلقوی رخ داده‌است. آلست و همکاران[23]، بن‌بست حلقوی را بدین صورت تعریف کرده‌اند: تعريف 8 (بن‌بست حلقوی): «بن‌بست حلقوی به معنای به دام افتادن یک مورد کاری (توکن) در یک چرخه‌ی بی‌پایان است.» در شکل 5 تبدیل یافته‌ی مدل فرآیندی ترسیم شده در شکل 4 بر اساس نگاشت ارائه شده در جدول 1 قابل مشاهده است. در این شکل، یک توکن در مکان شروع قرار دارد. با شلیک این توکن به وسیله‌ی انتقال Task1، فعالیت Task1 اجرا می‌شود. سپس، توکن به ترتیب توسط انتقال‌های Task2 و Task3 شلیک می‌شود تا در نهایت، در مکان خروجی انتقال Task3 (و ورودی انتقال split) واقع می‌شود. با فعال شدن انتقال split و شلیک شدن آن، یک توکن در مکان پایانی و یک توکن دیگر در مکان join قرار می‌گیرد. سپس برای توکن قرارگرفته در مکان join، مجددا به ترتیب توسط دو انتقال Task2 و Task3 و Split شلیک شده و مجددا در مکان Join قرار می‌گیرد؛ این چرخه مجددا و به تعداد دفعات نامتناهی تکرار می‌شود؛ در نتیجه، انتقال split به تعداد دفعات نامتناهی شلیک می‌شود و در نتیجه، تعداد توکن‌های موجود در مکان پایانی، به اندازه‌ی نامتناهی رشد خواهد کرد؛ ضمن این که انتقال‌های Task2 و Task3 نیز به تعداد دفعات نامتناهی شلیک می‌شوند و در نتیجه، این دو فعالیت به تعداد دفعات نامتناهی اجرا خواهند شد. شکل 5. تبدیل یافته‌ی مدل فرآیندی ترسیم شده در شکل 4 بر اساس نگاشت ارائه شده در جدول 1 با توجه به این که تعداد توکن‌های موجود در مکان پایانی به تعداد دفعات نامتناهی رشد می‌کند، شرط کراندار بودن در این شبکه‌ی پتری نقض می‌شود؛ در نتیجه این شبکه‌ی پتری، یک شبکه‌ی پتری صحیح نخواهد بود. 2- روش پیشنهادی 2-1- چارچوب کلي راه حل پيشنهادي رويکرد اصلي در اين تحقيق براي ارائه‌ي تعاريف پيشنهادي و نشان دادن درستي آن‌ها، استفاده از اثبات رياضي است. به منظور تعمیم مفهوم صحت به مدل‌های فرآیندی BPMN2.0، لازم است در ابتدا، ویژگی‌های اساسی یک فرآیندی صحیح، یعنی زنده بودن و کراندار بودن را از شبکه‌های پتری به آن تعمیم دهیم؛ بدين وسيله خواهيم دانست که اجزاي مدل فرآيندي BPMN به چه صورتي بايد در کنار يک ديگر قرار بگيرند تا مدل فرآيندي حاصل صحيح باشد؟ در ادامه، بعد از تعمیم این دو مفهوم به مدل‌های فرآیندی BPMN2.0، یک تعریف جامع برای یک مدل فرآیندی BPMN2.0 صحیح، ارائه خواهد شد. تعمیم این دو مفهوم بر مبنای دو اصل صورت می‌گیرد: 1. بر اساس تعريف 1 مدل‌هاي فرآيندي BPMN و فرآيندهاي ايجاد شده به وسيله‌ي شبکه‌هاي پتري، همگي مدل‌هايي فرآيندي هستند. 2. در بين مدل‌هاي فرآيندي BPMN و شبکه‌هاي پتري، ساختارهايي که داراي الگوهاي جريان کنترلي يکسان هستند، با رعايت نگاشت پيشنهاد شده توسط داکمن[13] مي‌توانند به يک ديگر نگاشته شوند. در بخش‌های بعدی، در ابتدا مفهوم کراندار بودن و سپس مفهوم زنده بودن را از شبکه‌های پتری به مدل‌های فرآیندی BPMN تعمیم می‌دهیم و با تعمیم این دو ویژگی مفهوم صحت ساختاري را بر اساس این دو مفهوم تعمیم یافته، به مدل‌های فرآیندی BPMN2.0 تعمیم می‌دهیم. رويکرد پيشنهادي در شکل 6 به تصوير کشيده شده‌است؛ در اين شکل، مستطيل‌هاي خاکستري نشان‌دهنده‌ي تعاريف مختص شبکه‌هاي پتري است که تحت نگاشت ارائه شده توسط داکمن به تعاريف پيشنهادي اين تحقيق تبديل شده‌است؛ همچنين مستطيل‌هاي سفيد، تعاريف پيشنهادي ارائه شده توسط اين تحقيق را نشان مي‌دهد که بر پايه‌ي تعاريف حاکم بر شبکه‌هاي پتري و نگاشت ارائه شده توسط داکمن ارائه شده‌است. شکل 6. شمايي از به کارگيري نگاشت ارائه شده توسط[13] به منظور تعميم مفاهيم کراندار بودن، زنده بودن و صحت 2-2- تعميم مفهوم کراندار بودن به مدل‌هاي فرآيندي BPMN در بخش 1-2-3-، یک مدل فرآیندی ایجاد شده به وسیله‌ی یک شبکه‌ی پتری را صحیح دانستیم، اگر و تنها اگر زنده و کراندار باشد و در همان بخش گفته شده که یک شبکه‌ی پتری کراندار است، اگر و تنها اگر رشد تعداد توکن‌های موجود در تمامی مکان‌های آن محدود باشد؛ این به این معناست که تعداد توکن‌های موجود در مکان‌های آن، به صورت نامتناهی رشد نمی‌کند. با توجه به این که پیش از هرکدام از مکان‌های شبکه‌های پتری (بجز مکان آغازین و پس از مکان پایانی)، یک انتقال وجود دارد و توکن‌هاي ايجاد شده در مکان‌هاي آن، در اثر شليک انتقال واقع شده در قبل از آن به وجود مي‌آيند، مي‌توان قضيه‌ي زير را در اين خصوص بيان نمود: قضيه 1 يک شبکه‌ي پتري کراندار است، اگر و تنها اگر تمامي انتقال‌هاي آن به تعداد دفعات متناهي شليک شوند. درستی این قضیه، بر اساس تعریف کراندار بودن[24] (بر اساس تعريف 4 ) قابل پذیرش است. حال، اگر يک مدل فرآيندي به وسيله‌ي شبکه‌هاي پتري مدل‌سازي شود، مي‌دانيم که فعاليت‌هاي آن، بخشی از انتقال‌های آن را تشکیل خواهند داد (طبق جدول 1)؛ در نتيجه از منظر مدل‌هاي فرآيندي عام (بحث شده در بخش 1-2-1- و مشخص شده در ستون ابتدایی جدول 1) بخشی از انتقال‌هاي يک شبکه‌ي پتري، مدل‌هاي فعاليتي يک مدل فرآيندي را تشکيل مي‌دهند و شليک آن‌ها به معناي اجراي آن فعاليت مي‌باشد؛ از سوي ديگر در زبان مدل‌سازي BPMN اين مدل‌هاي فعاليتي (از ديدگاه عام) در قالب فعاليت‌ها (مستطيل‌ها) نشان داده مي‌شوند و همان‌طور که در جدول 1 نشان داده شده‌است، مدل‌هاي فعاليتي در مدل‌هاي فرآيندي BPMN و در شبکه‌هاي پتري می‌توانند به یکدیگر نگاشته شوند. بنابراين مي‌توان مفهوم کراندار بودن را در مدل‌هاي فرآيندي BPMN به صورت زير تعريف نمود: تعريف 9 (کراندار بودن در مدل‌هاي فرآيندي BPMN) يک مدل فرآيندي BPMN2.0 را کراندار مي‌ناميم، اگر و تنها اگر تمامي فعاليت‌هاي آن (و یا رخدادهای آن) به تعداد دفعات متناهي اجرا شوند و در نتيجه، فاقد بن‌بست حلقوي و يا خطاهاي ناشي از آن، باشند. بر اساس این تعریف، نمونه‌هایی از مصادیق بن‌بست حلقوی می‌تواند شامل موارد زیر باشد: 1. وجود حلقه‌هاي اجرايي نامتناهي. 2. وجود بخش‌هايي از يک مورد کاري در سطح فرآيند، پس از اتمام آن. 3. وجود ارجاع‌هايي به يک مورد کاري پايان يافته در سطح فرآيند. در ادامه نشان مي‌دهيم که صادق بودنِ تعريف 9 در خصوص يک مدل فرآيندي BPMN2.0، معادل با کراندار بودن شبکه‌ي پتري معادلش است (طبق نگاشت ارائه شده در جدول 1). قضيه 2 يک مدل فرآيندي BPMN2.0، کراندار است، اگر و تنها اگر شبکه‌ي پتري معادل با آن، کراندار باشد. برهان: فرض کنيد به همین ترتیب نیز می‌توان گره‌های شبکه‌های پتری (که مشتمل بر انتقال‌ها و مکان‌ها هستند) را نیز به صورت زیر افراز نمود: با توجه به این که در شبکه‌های پتری، فعالیت‌ها و رخدادهای میانی با انتقال‌ها نشان داده می‌شوند (فعالیت‌ها و رخدادهای میانی، بخشی از انتقال‌ها را نشان می‌دهند) برای فعالیت‌ها خواهیم داشت: و برای رخدادهای میانی و آغازین نیز خواهیم داشت: ( در خصوص مدل‌های دروازه‌ای در شبکه‌های پتری، طبق جدول 1 مشاهده کردیم که برخی از دروازه‌ها با انتقال‌ها و برخی دیگر با مکان‌ها مدل‌سازی می‌شوند؛ بنابراین در خصوص مدل‌های دروازه‌ای داریم: به عنوان فرض خلف، فرض کنيد که مدل براي اثبات سمت ديگر قضيه، به عنوان فرض خلف، فرض کنيد که · اگر t تبديل يافته‌ي يک فعاليت مثل · اگر t تبديل يافته‌ي يک دروازه‌ي موازي موازي مثل بنابراين، فرض خلف باطل و حکم برقرار است. 2-3- تعميم مفهوم زنده بودن به مدل‌هاي فرآيندي BPMN در بخش 1-2-3- گفته شد که یک شبکه‌ی پتری زنده است، اگر و تنها اگر تمامي انتقال‌هاي آن، در وضعيتي شليک شوند؛ در چنين شبکه‌اي، انتقالي وجود ندارد که در هيچ وضعيتي شليک نشود؛ در نتيجه بن‌بست و تمامي خطاهاي مشابه آن (نظير وظايف مرده) در آن اتفاق نمي‌افتد. نتيجه 1: در صورتي که يک فرآيند سازماني ترسيم شده با شبکه‌ي پتري زنده باشد، فعاليتي در آن وجود ندارد که اجرا نشود. حال، اگر يک مدل فرآيندي به وسيله‌ي شبکه‌هاي پتري مدل‌سازي شود، انتقال‌هاي آن بيانگر فعاليت‌هاي آن فرآيند خواهند بود؛ در نتيجه از منظر مدل‌هاي فرآيندي عام (بحث شده در بخش 1-2-1-) انتقال‌هاي يک شبکه‌ي پتري، مدل‌هاي فعاليتي آن مدل فرآيندي را تشکيل مي‌دهند و شليک آن‌ها به معناي اجراي آن فعاليت مي‌باشد؛ از سوي ديگر در زبان مدل‌سازي BPMN اين مدل‌هاي فعاليتي (از ديدگاه عام) در قالب فعاليت‌ها (مستطيل‌ها) نشان داده مي‌شوند و همان‌طور که در جدول 1 نشان داده شده‌است، مدل‌هاي فعاليتي در مدل‌هاي فرآيندي BPMN و شبکه‌هاي پتري به يک ديگر نگاشته مي‌شوند. بنابراين مي‌توان مفهوم زنده بودن را در مدل‌هاي فرآيندي BPMN به صورت زير تعريف نمود: 1. وجود وظايف مرده (وظايفي که هرگز اجرا نمي‌شوند). 2. وجود فعاليت‌هايي که ورودي و يا خروجي نباشند. در ادامه، نشان مي‌دهيم که تعريف 10 ، تعريفي درست است؛ براي اين منظور نشان مي‌دهيم که يک مدل فرآيندي BPMN زنده است، اگر و تنها اگر شبکه‌ي پتري معادل آن (تحت نگاشت ارائه شده در جدول 1) زنده باشد. قضيه 3 يک مدل فرآيندي BPMN2.0 (طبق تعريف 10 ) زنده است، اگر و تنها اگر شبکه‌ي پتري معادل با آن، زنده باشد. برهان: فرض کنيد با توجه به این که هردو مدل، مدل‌هایی فرآیندی هستند می‌توان گره‌های آن‌ها را به سه زیرمجموعه‌ی مدل‌های فعالیتی (با زیروند A)، رخدادی (با زیروند E) و دروازه‌ای (با زیروند G) تقسیم نمود. بنابراین خواهیم داشت: به همین ترتیب نیز می‌توان گره‌های شبکه‌های پتری (که مشتمل بر انتقال‌ها و مکان‌ها هستند) را نیز به صورت زیر افراز نمود: با توجه به این که در شبکه‌های پتری، فعالیت‌ها و رخدادهای میانی با انتقال‌ها نشان داده می‌شوند برای فعالیت‌ها خواهیم داشت: و برای رخدادهای میانی و آغازین نیز خواهیم داشت: ( در خصوص مدل‌های دروازه‌ای در شبکه‌های پتری، طبق جدول 1 مشاهده کردیم که برخی از دروازه‌ها با انتقال‌ها و برخی دیگر با مکان‌ها مدل‌سازی می‌شوند؛ بنابراین در خصوص مدل‌های دروازه‌ای داریم: به عنوان فرض خلف، فرض کنيد که مدل · اگر t تبديل يافته‌ي يک فعاليت مثل · اگر t تبديل يافته‌ي يک دروازه‌ي موازي (انشعابي و يا اتصالي) باشد (در این صورت از سوي ديگر، براي اثبات سمت ديگر قضيه، به عنوان فرض خلف، فرض کنيد که · فعاليتی مثل · رخدادی مثل · دروازه‌ی اتصال موازی مثل 2-4- تعميم مفهوم صحت به مدل‌هاي فرآيندي BPMN در بخش‌هاي قبل، دو مفهوم زنده بودن و کراندار بودن را براي مدل‌هاي فرآيندي BPMN2.0، تعميم داديم و نشان داديم که اين دو مفهوم، معادل با مفاهيم کراندار بودن و زنده بودن شبکه‌هاي پتري معادل با آن مدل فرآيندي است؛ وجود هر يک از اين خواص در مدل‌هاي فرآيندي BPMN2.0، متضمن عدم وجود بخشي از خطاهاي ساختاري در آن خواهد بود. براي تعميم مفاهيم زنده بودن و کراندار بودن، از مفهوم علم مدل‌هاي فرآيندي و نيز، از نگاشت ارائه شده توسط داکمن [13] استفاده کرديم. همان‌طور که در بخش 1-2-3- مشاهده شد، صحت يک مدل فرآيندي ترسيم شده با استفاده از شبکه‌هاي پتري، مستلزم برقراري دو شرط زنده بودن و کراندار بودن است. در بخش‌هاي 2-2- و 2-3- به ترتيب مفاهيم کراندار بودن و زنده بودن را با استفاده از نگاشت ارائه شده توسط داکمن و نيز مفهوم عام مدل‌هاي فرآيندي، به مدل‌هاي BPMN تعميم داديم و ضمن ارائه‌ي تعاريف مجزا براي کراندار بودن و زنده بودن مدل‌هاي فرآيندي BPMN، در قضيه 2 و قضيه 3 نشان داديم کراندار بودن و زنده بودن يک مدل فرآيندي، با کراندار بودن و زنده بودن شبکه‌ي پتري معادل با آن، معادل است. حال، لازم است مفهوم نهايي صحت را نيز بر مبناي تعاريف زنده بودن و کراندار بودن، به مدل‌هاي فرآيندي BPMN تعميم دهيم. بنابراين تعريف زير را براي يک مدل فرآيندي BPMN صحيح پيشنهاد مي‌کنيم: تعريف 11 يک مدل فرآيندي BPMN2.0 صحيح است، اگر و تنها اگر کراندار (طبق تعريف 9 ) و زنده (طبق تعريف 10 ) باشد. تعريف 11 بيان مي‌دارد که يک مدل فرآيندي BPMN2.0 سالم است، اگر و تنها اگر فاقد بن‌بست و خطاهاي ناشي از آن و نيز، فاقد بن‌بست حلقوي و خطاهاي ناشي از آن باشد. به منظور اثبات اين ادعا، قضيه‌ي زير را مطرح مي‌کنيم: رديف شاخص/ خطاي ساختاري مورد بحث شاخص مرتبط بر اساس تعاريف پيشنهادي تحقيقات مرتبط 1 امن بودن کراندار بودن [10]،[1] 2 کشف بن‌بست حلقوي کراندار بودن [14]، [6]، [18]،[6]، [7] 3 کشف حلقه‌هاي بي‌نهايت کراندار بودن [14] 4 کشف نقاط گلوگاهي زنده بودن [16] 5 بررسي دسترسي‌پذيري زنده بودن [13]،[15]، [14]،[17] 6 بررسي احتمال وقوع بن‌بست زنده بودن [9] 7 کشف بن‌بست زنده بودن [10]،[1]، [13]،[14] [17]،[16]، [6]، [18]، [6]، [7]، [8]، [25] 3-3- ارزيابي روش‌هاي پيشنهادي صحت‌سنجي ساختاري بر اساس تعاريف پيشنهادي در جدول 3 فهرستي از تحقيقات صورت گرفته در حوزه‌ي صحت‌سنجي مدل‌هاي فرآيندي BPMN وجود دارد؛ در اين جدول مشخص شده‌است که هرکدام از کارهاي قبلي با در نظر گرفتن کدام يک از خطاهاي ساختاري و يا کدام يک از شاخص‌هاي صحت ساختاري، اقدام به صحت‌سنجي مدل‌هاي فرآيندي کرده‌اند؛ چنانچه حداقل يکي از ويژگي‌هاي کراندار بودن و حداقل يکي از ويژگي‌هاي زنده بودن در خصوص يک روش صحت‌سنجي قابل بررسي باشد، بر طبق تعريف 11 و قضيه 4، تمامي جنبه‌هاي صحت (یعنی زنده بودن وکران‌دار بودن مدل فرآیندی) توسط آن روش پيشنهادي، پوشش داده شده‌است (و اين موضوع در آخرين ستون جدول 3 بيان شده‌است)؛ اما اين موضوع به اين معنا نيست که آن روش، صحت ساختاري را به صورت 100 درصد مي‌تواند تضمين کند؛ چرا که ممکن است ويژگي‌هاي مورد بررسي، فقط بخشی از خطاهای ساختاری ناقض زنده بودن و یا کراندار بودن را پوشش دهد؛ بنابراين روش‌هايي به صورت قطعي قابل اتکا هستند که کراندار بودن و زنده بودن را در حالت کلي و بر طبق تعريف 9 و تعريف 10 تضمين نمايند؛ اين موضوع تا حد خيلي خوبي در تحقيقات صورت گرفته توسط فلاويو کورديني و نيون رعايت شده‌است و زنده بودن در حالت کلي درنظر گرفته شده‌است؛ همچنين، در اين دو کار تحقيقاتي شاخص امن بودن نيز در نظر گرفته شده‌است که حالت خاصي از کراندار بودن است (طبق تعريف 5 و تعريف 6 ). جدول 3. ارزيابي خطاهاي مورد بررسي در تحقيقات پيشين بر مبناي تعاريف پيشنهادي روش پيشنهاد شده بررسي زنده بودن بررسي کراندار بودن آيا تمامي جنبه‌هاي صحت پوشش داده شده است؟ کشف بن‌بست بررسي احتمال وقوع بن‌بست بررسي دسترسي پذيري کشف نقاط گلوگاهي کشف حلقه‌هاي بي نهايت کشف بن‌بست حلقوي امن بودن داکمن (2008): استفاده از شبکه‌هاي پتري کلاسيک [13] * * خير تاکمورا (2008): استفاده از شبکه‌هاي پتري کلاسيک براي صحت‌سنجي تراکنش‌هاي ايجاد شده با استاندارد BPMN [15] * خير او يانگ (2008): استفاده از شبکه‌هاي پتري کلاسيک[14] * * * * بله وانگ (2011): استفاده از منطق زماني خطي (LTL) [17] * * خير واتاهيکي (2011): وارسي مدل و سپس تصديق آن با ابزار UPPAL با فرض وجود محدوديت زماني و منابع در فرآيند [16]. * * خير خربوشه (2012): استفاده از وارسي مدل، نگاشت مدل فرآيندي به ساختار کريپکي و استفاده از منطق زماني خطي (LTL) [6]. * * بله فالسيوني (2012): ارائه‌ي يک الگوريتم Unfolding براي بررسي اثرات مخرب فرآيند [18]. * * بله خربوشه (2013): بهبود تحقيق پيشين (تحقيق [6]) [7]. * * بله پرينز (2014): ارائه‌ي يک مدل به نام گراف جريان کار به منظور ايجاد يک کامپايلر براي مدل‌هاي فرآيندي BPMN [8]. * خير الحکمي و نوم (2015): استفاده از ساختار جبري ماکس پلاس [25]. * خير نوم و الحکمي (2017): يک روش صحت‌سنجي و مبتني بر ضرب احتمالات [9] * خير فلاويو کورديني (2021): در پایان و در نتایج این مقاله، مشخص شده‌است که صحیح نبودن یک فرآیند، لزوما امن بودن آن را نقض نمی‌کند؛ اما در صورتی که یک مدل فرآیندی خوش‌ساختار باشد، الزاما صحیح و امن است [10]. اين کار تحقيقاتي بر اساس انواع خاصي از خطاهاي ساختاري پيش برده نشده‌است و ابعاد صحت به صورت صوري و با تعاريفي کلي مورد ارزيابي قرار مي‌گيرد. * بله نيون و همکاران (2022): عمده‌ی هدف این مقاله معطوف بر تصدیق ویژگی زنده بودن در مدل‌های فرآیندی BPMN است. با این حال،در این مقاله به مفهوم امن بودن مدل فرآیندی نیز توجه شده‌است که در این صورت، به تصدیق ویژگی کراندار بودن نیز منجر می‌گردد؛ در نتیجه بر اساس شاخص‌های پیشنهادی ما، این کار تحقیقاتی نیز تمامی جنبه‌های صحت ساختاری را پوشش میدهد [1]. اين کار تحقيقاتي بر اساس انواع خاصي از خطاهاي ساختاري پيش برده نشده‌است و ابعاد صحت به صورت صوري و با تعاريفي کلي مورد ارزيابي قرار مي‌گيرد. * بله 4- نتيجهگيري در اين مقاله، معناي يک مدل فرآيندي صحيح را در زبان BPMN تعريف کرديم (تعريف 11 )؛ صحيح بودن يک مدل فرآيندي BPMN مستلزم زنده بودن و کراندار بودن آن است. زنده بودن يک مدل فرآيندي BPMN متضمن اجراي تمامي فعاليت‌ها و رخدادهاي آن است و کراندار بودن آن متضمن اجراي تمامي فعاليت‌ها و رخدادهاي آن به تعداد دفعات متناهي است. درستي اين تعاريف در قالب قضيه 3 و قضيه 2 بر پايه‌ي شبکه‌هاي پتري و مفهوم عام مدل‌هاي فرآيندي اثبات شد و در نهايت در قضيه 4 اثبات شد که تعريف پيشنهادي در خصوص صحت مدل‌هاي فرآيندي BPMN با مفهوم صحت در معادل آن مدل فرآيندي در شبکه‌هاي پتري، هم‌ارز است. در پايان، شاخص‌هاي مورد بررسي توسط تحقيقات پيشين را بر اساس تعاريف پيشنهادي زنده بودن و کراندار بودن در قالب جدول 2 طبقه‌بندي کرده و بر مبناي آن، در جدول 3 تحقيقات پيشين بر مبناي پوشش دادن دو ويژگي زنده بودن و کراندار بودن، دسته‌بندي شدند. در نتيجه‌ي آن مي‌توان مشاهده کرد که بسياري از تحقيقات پيشين منحصرا يکي از جنبه‌هاي يک مدل فرآيندي صحيح را پوشش داده‌اند و در نتيجه، نمي‌توانند صحت ساختاري يک مدل فرآيندي BPMN را تضمين کنند؛ اما در تحقيقات اخير همانند تحقيقات فلاويو کورديني [10] و نيون [1] ضمن پوشش هر دو جنبه‌ي صحت ساختاري، اين دو شاخص در حالت کلي و فارغ از نوع خطاي ساختاري مد نظر قرار گرفته‌است؛ در نتيجه بر مبناي تعاريف پيشنهادي در اين پژوهش، روش پيشنهادي در اين دو تحقيق مي‌تواند صحت ساختاري اين مدل‌هاي فرآيندي را تضمين نمايد. سپاسگزاری از دست اندرکاران برگزاري پنجمين همايش ملي معماري سازماني (پاييز 1400 در دانشگاه فردوسي مشهد و با نظارت آزمايشگاه معماري سازماني دانشگاه شهيد بهشتي) بابت داوري و تاييد نسخه‌ي اوليه‌ي اين مقاله [26]سپاس گزاريم و در پايان از اساتيد ارجمند، جناب آقاي دکتر کمندي (استادیار گروه علوم مهندسی دانشگاه تهران) و جناب آقای دکتر اکبر مصطفوی (استادیار گروه مهندسی کامپیوتر دانشگاه یزد) بابت بیان نکات ارزشمندشان در نشست ارائه‌ی مقاله، سپاس‌گزاریم. مراجع [1] Q. Nivon and G. Salaün, "Debugging of BPMN Processes Using Coloring Techniques," in Formal Aspects of Component Software, Cham, S. L. Tapia Tarifa and J. Proença, Eds., 2022// 2022: Springer International Publishing, pp. 90-109. [2] F. Huang, F. Ni, J. Liu, F. Yang, and J. Zhu, "A Colored Petri Net Executable Modeling Approach for a Data Flow Well-Structured BPMN Process Model," IEEE Access, vol. 10, pp. 86696-86709, 2022, doi: 10.1109/ACCESS.2022.3198969. [3] Y. Poursoltani, M. H. Shirali-Shahreza, and S. A. Hashemi Golpayegani, "Using Low-Code Development Platforms for developing Commercial Software based on Business Processes (wrote In Persian)," presented at the Conference: 26th International Computer Conference, Computer Society of Iran, Iran - Tehran, 1399 (In Persian). [Online]. Available: https://civilica.com/doc/1203571. [4] R. Waszkowski, "Low-code platform for automating business processes in manufacturing," IFAC-PapersOnLine, vol. 52, no. 10, pp. 376-381, 2019/01/01/ 2019, doi: https://doi.org/10.1016/j.ifacol.2019.10.060. [5] S. Braams, "Developing a Software Quality Framework for Low-Code Model Driven Development Platforms Based on Behaviour Driven Development Methodology.," presented at the 27th Twente Student Conference on IT, Enschede, The Netherlands., July 7th, 2017, 2017. [6] O. M. Kherbouche, A. Ahmad, and H. Basson, "Detecting structural errors in BPMN process models," in 2012 15th International Multitopic Conference (INMIC), 2012: IEEE, pp. 425-431. [7] O. M. Kherbouche, A. Ahmad, and H. Basson, "Using model checking to control the structural errors in BPMN models," IEEE 7th International Conference on Research Challenges in Information Science (RCIS), pp. 1-12, 2013. [8] T. M. Prinz, N. Spieß, and W. Amme, "A First Step towards a Compiler for Business Processes," Berlin, Heidelberg, 2014: Springer Berlin Heidelberg, in Compiler Construction, pp. 238-243. [9] M. Naoum, O. E. Hichami, M. A. Achhab, and B. E. E. Mohajir, "A probabilistic method for business process verification: Reachability, Liveness and deadlock detection," 2016 4th IEEE International Colloquium on Information Science and Technology (CiSt), pp. 128-132, 2016. [10] F. Corradini, A. Morichetta, C. Muzi, B. Re, and F. Tiezzi, "Well-structuredness, safeness and soundness: A formal classification of BPMN collaborations," Journal of Logical and Algebraic Methods in Programming, vol. 119, p. 100630, 2021/02/01/ 2021, doi: https://doi.org/10.1016/j.jlamp.2020.100630. [11] S. Meghzili, A. Chaoui, M. Strecker, and E. Kerkouche, "An Approach for the Transformation and Verification of BPMN Models to Colored Petri Nets Models," International Journal of Software Innovation (IJSI), vol. 8, no. 1, pp. 17-49, 2020, doi: 10.4018/IJSI.2020010102. [12] M. Weske, "Business Process Modelling Foundation," in Business Process Management: Concepts, Languages, Architectures. Berlin, Heidelberg: Springer Berlin Heidelberg, 2012, pp. 73-124. [13] R. M. Dijkman, M. Dumas, and C. Ouyang, "Semantics and analysis of business process models in BPMN," Information and Software Technology, vol. 50, no. 12, pp. 1281-1294, 2008/11/01/ 2008, doi: https://doi.org/10.1016/j.infsof.2008.02.006. [14] C. Ou-Yang and Y. Lin, "BPMN-based business process model feasibility analysis: a petri net approach," International Journal of Production Research, vol. 46, no. 14, pp. 3763-3781, 2008. [15] T. Takemura, "Formal Semantics and Verification of BPMN Transaction and Compensation," in 2008 IEEE Asia-Pacific Services Computing Conference, 9-12 Dec. 2008 2008, pp. 284-290, doi: 10.1109/APSCC.2008.208. [16] K. Watahiki, F. Ishikawa, and K. Hiraishi, "Formal verification of business processes with temporal and resource constraints," in 2011 IEEE International Conference on Systems, Man, and Cybernetics, 9-12 Oct. 2011 2011, pp. 1173-1180, doi: 10.1109/ICSMC.2011.6083857. [17] J. G. Peter Y.H. Wong, "Property specifications for workflow modelling," Science of Computer Programming, vol. 76, no. 10, pp. 942-967, 2011, doi: https://doi.org/10.1016/j.scico.2010.09.007. [18] D. Falcioni, A. Polini, A. Polzonetti, and B. Re, "Livelock and Deadlock Detection for PA Inter-organizational Business Processes," in Advancing Democracy, Government and Governance, Berlin, Heidelberg, A. Kő, C. Leitner, H. Leitold, and A. Prosser, Eds., 2012// 2012: Springer Berlin Heidelberg, pp. 125-139. [19] O. M. Kherbouche, A. Ahmad, and H. Basson, "Using model checking to control the structural errors in BPMN models," in IEEE 7th International Conference on Research Challenges in Information Science (RCIS), 29-31 May 2013 2013, pp. 1-12, doi: 10.1109/RCIS.2013.6577723. [20] G. Barbon, V. Leroy, and G. Salaün, "Debugging of concurrent systems using counterexample analysis," in Fundamentals of Software Engineering: 7th International Conference, FSEN 2017, Tehran, Iran, April 26–28, 2017, Revised Selected Papers 7, 2017: Springer, pp. 20-34. [21] O. El Hichami, M. Naoum, M. Al Achhab, I. Berrada, and B. E. El Mohajir, "An Algebraic Method for Analysing Control Flow of BPMN Models," International Journal of Recent Contributions from Engineering, Science & IT (iJES), vol. 3, no. 3, pp. pp. 20-26, 10/19 2015, doi: 10.3991/ijes.v3i3.4862. [22] G. Decker, R. Dijkman, M. Dumas, and L. García-Bañuelos, "The Business Process Modeling Notation," in Modern Business Process Automation: YAWL and its Support Environment, A. H. M. Hofstede, W. M. P. Aalst, M. Adams, and N. Russell Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 2010, pp. 347-368. [23] W. v. d. A. a. K. v. H. The, Workflow Management. Models, Methods, and Systems. Massachusetts London,England: MIT Press Cambridge, 2002. [24] R. Zurawski and M. Zhou, "Petri nets and industrial applications: A tutorial," IEEE Transactions on industrial electronics, vol. 41, no. 6, pp. 567-583, 1994. [25] O. E. Hichami, M. Naoum, M. A. Achhab, I. Berrada, and B. E. E. Mohajir, "An Algebraic Method for Analysing Control Flow of BPMN Models," Int. J. Recent Contributions Eng. Sci. IT, vol. 3, no. 3, pp. 20-26, / 2015. [Online]. Available: https://www.online-journals.org/index.php/i-jes/article/view/4862. [26] Y. Poursoltani, M. H. Shirali-Shahreza, and S. A. Hashemi Golpayegani, "Redefining the Soundness for BPMN2.0 Process Models, based on Petri nets," presented at the 5th National Conference on Advances in Enterprise Architecture (NCAEA), Mashhad- Iran, 2021. [Online]. (In Persian).Available: https://civilica.com/doc/1386000/. [1] Object Management Group (OMG) [2] Static Graph Oriented Language [3] Control Flow Errors [4] Data Flow Errors [5] Unit Testing [6] Dead Lock [7] Livelock [8] Source Process Models [9] Mapping Method [10] Target process Models [11] Structural Soundness Metrics [12] Model Driven Software Engineering (MDSE) [13] Liveness [14] Boundness [15] Reachability [16] Linear Temporal Time (LTL) [17] Unfolding [18] Collaborative Business Processes [19] Model Checking [20] Kripke [21] Linear Temporal Logic (LTL) [22] Workflow Graph [23] Model Checking [24] Model Checker [25] Labelled Transition Systems (LTS) [26] MAX – Plus [27] Likelihood [28] Collaborative Process Models [29] Soundness [30] Safeness [31] Well Structureness [32] Process Model [33] Activity Models [34] Activity Models [35] Activity Models [36] Workflow net [37] Start By Trigger [38] Sound [39] Live [40] Bound [41] Deadlock [42] Dead Tasks
که به واسطه‌ی شلیک انتقال‌ها از وضعیت اولیه‌ی 
قابل تولید باشد، با شلیک دنباله‌ای از انتقال‌ها بدست آید.»
(کراندار) می‌نامیم اگر و تنها اگر تعداد توکن‌های موجود در آن بیشتر از 
نشود.»
تعداد توکن‌هایی که در يک مکان مثل 
توليد مي‌شوند، محدود است و به صورت بي‌کران رشد نمي‌کند. با توجه به اين‌که پيش از هر مکان (بجز مکان شروع)، يک انتقال قرار دارد و توکن‌هاي داخل آن مکان، به واسطه‌ي شليک انتقال واقع در قبل از آن به وجود مي‌آيد، کراندار بودن بدان معنا خواهد بود که در چنين شبکه‌اي، انتقالي وجود نخواهد داشت که به تعداد دفعات نامتناهي شليک شود. کراندار بودن يک فرآيند، تضمين مي‌کند که در آن، فعاليتي وجود ندارد که با تعداد دفعات نامتناهي اجرا شود. اين ویژگی، عدم وجود حلقه‌هاي اجرايي نامتناهي و يا بن‌بست‌هاي حلقوي را تضمين مي‌کند.
بن‌بست را این‌گونه تعریف کردند:
در يک مدل فرآيندي BPMN
)، توسط اولین انتقال (انتقال Start Transition) به دومین مکان (مکان 
) شلیک شود، انتقال Task2 فعال خواهد شد، اما با توجه به این که هنوز توکنی در مکان خروجی Task2 واقع نیست، انتقال G فعال نمی‌شود. سپس با شلیک Task2، توکن از مکان دوم حذف خواهد شد و در مکان خروجی Task2 یک توکن قرار خواهد گرفت. با توجه به این که فقط یکی از ورودی‌های انتقال G فعال خواهد بود، این انتقال هیچگاه فعال نشده و شلیک نخواهد شد و در نتیجه یک بن‌بست در این انتقال رخ میدهد. نظر به این که وضعیتی رخ داده‌است که در آن G فعال نشده‌است، در این شبکه‌ی پتری، شرط زنده بودن نقض شده و در نتیجه، این مدل فرآیندی صحیح نمی‌باشد.
يک مدل فرآيندي BPMN2.0 باشد و ، شبکه‌ي پتري معادل با آن باشد که در اثر نگاشت ارائه شده در جدول 1 بدست آمده‌باشد. با توجه به این که هردو مدل، مدل‌هایی فرآیندی هستند (طبق تعریف 1) می‌توان گره‌های آن‌ها را به سه زیرمجموعه‌ی مدل‌های فعالیتی (با زیروند A)، رخدادی (با زیروند E) و دروازه‌ای (با زیروند G) تقسیم نمود. بنابراین خواهیم داشت:
و 
به ترتیب مکان‌های آغازین و پایانی هستند) در نتیجه، به طور کلی برای مدل‌های رخدادی در شبکه‌ی پتری 
خواهیم داشت:
(یک مدل فرآیندی BPMN است) بر طبق تعريف 9 کراندار باشد (يعني بر طبق تعريف ارائه شده، هر کدام از فعاليت‌هاي آن به تعداد دفعات متناهي اجرا شود و در نتيجه، فاقد بن‌بست حلقوي و خطاهاي مشتق شده از آن باشد) اما کراندار نباشد. در نتيجه، مکاني مانند در وجود خواهد داشت، به طوري‌که که تعداد توکن‌هايي که به آن وارد مي‌شود، تا حد بي‌کران رشد مي‌کند. بنابراين، يک انتقال مانند 
وجود خواهد داشت که پيش از مکان 
قرار دارد و با شليک شدن به تعداد دفعات نامتناهی، توکن‌هايي را به اين مکان وارد مي‌کند. اگر اين انتقال تبديل يافته‌ي يک رخداد و يا يک فعاليت باشد (طبق جدول 1)، در مدل فرآيندي يک فعاليتي مثل 
و يا رخدادي مثل 
وجود خواهد داشت که به تعداد دفعات نامتناهي اجرا شده‌است. درنتيجه، مدل فرآيندي کراندار نخواهد بود. در نتيجه فرض خلف باطل و حکم برقرار مي‌شود.
کراندار نباشد و در عين حال، کراندار باشد و فاقد بن‌بست حلقوي و يا تبعات آن باشد. اگر کراندار نباشد، يک مکان مثل در آن وجود خواهد داشت که تعداد نامتناهي توکن دريافت مي‌کند و اين توکن‌ها، در اثر شليک يک انتقالي مثل به وجود مي‌آيند؛ بنابراين، بر اساس انتقال t موارد زیر ممکن هستند:
و يا رخداد مثل 
باشد، بدان معنا خواهد بود که فعاليتa و يا رخداد e، با تعداد دفعات نامتناهي اجرا مي‌شوند که با کراندار بودن b (طبق جدول 1) در تناقض است.
باشد، بدان معنا خواهد بود که عمل موازي‌سازي و هم‌گام سازي در b بي نهايت مرتبه اجرا مي‌شود و اين امر نشان‌دهنده‌ي يک حلقه‌ي نامتناهي اجرايي در b است که با کراندار بودن آن، در تناقض است.
يک مدل فرآيندي BPMN2.0 باشد و ، شبکه‌ي پتري معادل با آن باشد که تحت نگاشت ارائه شده در جدول 1 بدست آمده‌باشد.
و به ترتیب مکان‌های آغازین و پایانی هستند). در نتیجه، به طور کلی برای مدل‌های رخدادی در شبکه‌ی پتری خواهیم داشت:
زنده باشد (يعني بر طبق تعريف 10 فاقد بن‌بست و يا تبعات آن باشد؛ بنابراین تمامی فعالیت‌های آن قابل اجرا بوده و تمامی رخدادهای آن نیز قابل وقوع خواهد بود) اما زنده نباشد؛ بنابراین، انتقالي مثل در آن وجود خواهد داشت، که شليک نمي‌شود. در اين صورت:
باشد (یعنی 
) و يا يک رخداد مثل در b باشد ( در این صورت 
)، فعاليت a و يا رخداد e در b وجود خواهد داشت، به طوري که اجرا نمي‌شود و اين اتفاق، با فرض زنده بودن b در تناقض است.
)، دروازه‌اي موازي مثل در مدل فرآيندي b وجود خواهد داشت، به طوري که جريان اجراي فرآيند، هيچ‌گاه از آن عبور نخواهد کرد. در نتيجه، b حاوي يک بن‌بست است و با فرض زنده بودن آن در تناقض است.
زنده باشد، اما زنده نباشد. در اين صورت بر طبق جدول 1 داریم:
در وجود خواهد داشت، به طوري که اجرا نمی‌شود. در نتيجه، انتقالي مثل
(معادل با آن فعاليت) در شبکه‌ي وجود خواهد داشت که تبديل يافته‌ي آن فعاليت است و شليک نمي‌شود و اين اتفاق، با زنده بودن شبکه‌ي در تناقض است. در نتيجه فرض خلف باطل و حکم، برقرار است.
در وجود خواهد داشت، به طوري که اجرا نمی‌شود. در نتيجه، انتقالي مثل
(معادل با آن رخداد) در شبکه‌ي وجود خواهد داشت که تبديل يافته‌ي آن فعاليت است و شليک نمي‌شود و اين اتفاق، با زنده بودن شبکه‌ي در تناقض است. در نتيجه فرض خلف باطل و حکم، برقرار است.
در وجود خواهد داشت، به طوري که حداقل یکی از ورودی‌های آن فعال نمی‌شود؛ در نتيجه، انتقالي مثل
(معادل با آن رخداد) در شبکه‌ي وجود خواهد داشت که تبديل يافته‌ي آن دروازه است و شليک نمي‌شود و اين اتفاق، با زنده بودن شبکه‌ي در تناقض است. در نتيجه فرض خلف باطل و حکم، برقرار است.
