Business Process Modeling — Alessandro Carella

This is my Business Process Modeling class project. The objective was to model and evaluate the procedural dynamics through which a painting school manages student requests, learning appointments, and pedagogical interactions between students and teachers.

The process encompasses the complete student lifecycle, from initial contact with the school through course selection, lesson scheduling, artistic session execution, feedback incorporation, and payment processing. The modeling effort employed two complementary approaches: Business Process Model and Notation (BPMN), through the use of Camunda Modeler, for visual process representation, and Workflow Nets (a specialized form of Petri nets) for formal mathematical analysis and verification.

The analysis utilized WoPeD, a specialized tool for Petri net modeling and analysis, to evaluate critical properties including soundness, boundedness, liveness, and deadlock-freeness. Both a base model and a variant supporting course renewal were developed and analyzed.

This project provided deep insights into formal methods for business process analysis and the critical importance of verification in process design. I learned how to translate real-world collaborative processes into rigorous formal models that can be mathematically verified.

The transformation from BPMN to Workflow nets taught me how different modeling paradigms complement each other, BPMN excels at stakeholder communication and visual clarity, while Petri nets enable behavioral analysis. I gained practical experience with the systematic transformation rules: replacing tasks and events with transitions, sequence flows with places, and properly handling gateway constructs.

Working with WoPeD deepened my understanding of workflow net properties. I learned to identify and interpret S-components, PT-handles, and TP-handles, and to recognize their implications for process structure. The analysis revealed how soundness, boundedness, and liveness properties ensure that processes can execute reliably without deadlocks or resource accumulation issues.

A significant learning came from analyzing free-choice violations in the integrated models. These violations, appearing where multiple actors coordinate through overlapping decision points, taught me about the complexity of multi-party processes and the trade-offs between model simplicity and realistic representation.

The project also demonstrated the value of variant analysis. By modeling both a base process and an extended version supporting course renewal, I learned how to assess the impact of process changes on structural properties and identify potential issues before implementation.

The BPMN model captures the collaborative choreography between two primary participants: the Student and the School. This dual-lane structure effectively separates responsibilities while maintaining clear communication pathways through message flows.

The Student lane has five major phases. The process begins with course selection, where the student contacts the school and receives available course options. Following selection, an iterative appointment scheduling loop ensures mutual agreement on lesson timing and location through exclusive gateways that handle proposal acceptance or counter-proposals. Prior to each lesson, students receive and review preparatory materials covering techniques and tools. During sessions, students create drafts under teacher guidance with opportunities for clarification. Post-session activities involve draft selection negotiation, finalization, digitization, and submission, followed by electronic payment and the decision to continue with another appointment or terminate the course.

The School lane mirrors these interactions from the institutional perspective. It manages course offerings and teacher assignments, participates in the bidirectional appointment negotiation loop, prepares and distributes lesson materials, provides active supervision and instruction during sessions, proposes draft selections for finalization, verifies payments, and responds to student decisions regarding course continuation or closure.

Message flows between lanes capture critical synchronization points including course initiation requests, scheduling negotiations, material transmissions, feedback exchanges, draft selection discussions, submission and payment confirmations, and closure decisions. This comprehensive message-based coordination ensures both parties remain synchronized throughout the process lifecycle.

The transformation from BPMN to Workflow nets followed established conversion principles. Each task and event was replaced with a transition, each sequence flow became a place, XOR splits and joins were translated into combinations of places and transitions, and event-based gateways were represented as places followed by alternative transitions. Critically, single initial and final places were added to satisfy the formal definition of a Workflow Net.

The Student Workflow net comprises 37 places, 42 transitions, and 84 arcs, forming a single connected and strongly connected component of 79 nodes. Analysis confirmed it is S-coverable with one comprehensive S-component, well-structured with no PT or TP handles, and satisfies all soundness properties. The net proved to be bounded, live, and correctly initialized, ensuring reliable execution without deadlocks or resource issues.

The School Workflow net contains 31 places, 36 transitions, and 72 arcs, totaling 67 nodes in a single connected component. It similarly demonstrates S-coverability, well-structuredness, soundness, boundedness, and liveness, confirming the institutional process logic is formally correct and executable.

The complete integrated model, merging all perspectives, consists of 88 places, 78 transitions, and 198 arcs. While maintaining fundamental soundness properties, one source place, one sink place, no non-standard arc weights, proper connectivity, the integration introduced six free-choice violations at points of overlapping communication or decision-making. These violations, occurring in clarification exchanges, counter-offer handling, draft negotiations, and course notifications, reflect the inherent complexity of coordinated multi-actor processes. The model contains 444 S-components, 228 PT-handles, and 210 TP-handles, indicators of structural complexity that suggest opportunities for future refinement while not compromising functional correctness.

The variant model extends the base process by enabling students to initiate new courses upon completing their current enrollment, creating a recursive educational trajectory. This modification required careful additions to both lanes while preserving process soundness.

In the Student lane, an exclusive gateway was inserted after the course completion notification event. This gateway routes process control either to termination or, if the student opts for a new course, back to the course selection phase through a message flow to the School. Correspondingly, the School lane received an event-based gateway following completion message reception. This gateway waits for either a new course notification or proceeds to termination if no such message arrives, with the new course path looping back to await the student's course choice.

The variant complete model contains 93 places, 83 transitions, and 212 arcs across 176 connected nodes. It maintains soundness, boundedness, and liveness but exhibits seven free-choice violations, one more than the base model, reflecting the additional decision complexity introduced by the renewal option. The model comprises 270 S-components, 308 PT-handles, and 276 TP-handles, representing increased structural complexity that accompanies the enhanced flexibility. Despite these metrics, the variant preserves all fundamental execution correctness properties, demonstrating that the process extension was implemented soundly.

The verification process examined multiple critical properties that ensure process correctness. Soundness verification confirmed that all models possess exactly one source place and one sink place, have no transitions with empty presets or postsets, and form single connected components, guaranteeing that every part of the process is reachable and properly terminates.

Boundedness analysis proved that no place, in any model, can accumulate an infinite number of tokens, preventing resource accumulation problems. This property is essential for ensuring that the process can execute repeatedly without exhausting system resources.

Liveness verification confirmed that no transitions are dead or non-live, meaning every activity in the process can potentially execute in some reachable state. This ensures that no part of the modeled process becomes permanently unreachable during execution, a critical property for operational reliability.

S-component analysis revealed interesting differences between individual and integrated models. The individual student and school models each contain single comprehensive S-components covering all nodes, indicating tight behavioral cohesion. In contrast, the integrated models contain hundreds of S-components (444 in the base model, 270 in the variant), reflecting the distributed nature of collaborative processes where multiple concurrent paths exist.

Well-structuredness assessment identified PT-handles and TP-handles in the integrated models. While these structural patterns don't compromise soundness, their presence indicates areas where control flow branching creates complexity. The 228 PT-handles and 210 TP-handles in the complete model suggest opportunities for future process simplification and improved modularity.

Free-choice violation analysis uncovered coordination points where transitions share input places without maintaining independent choice sets. These six violations in the base model and seven in the variant occur at natural collaboration points, clarification exchanges, offer negotiations, draft selections, and course notifications, representing the fundamental complexity of multi-party coordination rather than modeling errors.