Three roles, one internship.
The workflow follows an internship from the first interview to the final employment decision, across three participants who only coordinate through messages:
Conducts the interview, assigns the intern to a work group, receives the final evaluation and decides whether to offer a job contract.
Contacts the project leader, receives activities and deadlines, performs the work and submits reports.
Matches activities to the intern's competencies, sets deadlines, evaluates reports and manages the remaining internship time.
Connect the three pools in the baseline collaboration, with competence-checking loops, repeated assignments and deadline signals.
From diagrams to formal models.
BPMN is great for people; verification needs a formal model. I translated the process into three views: the BPMN collaboration, one workflow net per role, and a composed system where communication places connect the roles and a final synchronization transition waits for all three to finish before marking the common end. Global completion becomes an explicit modeling decision.
| Workflow net | Baseline: places / transitions / arcs | Extended: places / transitions / arcs |
|---|---|---|
| Supervisor | 6 / 6 / 12 | 9 / 10 / 20 |
| Intern | 11 / 11 / 22 | 14 / 15 / 30 |
| Project leader | 20 / 22 / 44 | 24 / 28 / 56 |
| Composed system | 44 / 39 / 96 | 57 / 50 / 128 |
Counts from the WoPeD net statistics. The demo at the top plays the baseline composed system, read directly from its PNML file.
Coordinating a restart.
The variant adds a business decision: after the final evaluation, the Supervisor can extend the internship. That one decision needs a coordination protocol:
- The Supervisor announces the extension to both the Intern and the Project leader.
- Both acknowledge that they are ready to continue.
- The composed net synchronizes the Supervisor's continuation with both acknowledgements: the restart transition needs three input places at once.
- The internship resumes from the work-group assignment.
The cost is visible in the models: the BPMN collaboration grows from 9 to 15 message flows, the composed net from 44 to 57 places and from 39 to 50 transitions.
Sound, before and after.
A workflow net is sound when three things hold: every reachable state can still reach the end (option to complete), reaching the end leaves no stray tokens (proper completion), and every task can actually happen (no dead transitions). The analysis was run in WoPeD on every net, together with coverability graphs and S-component coverage for the single roles.
| Composed system | Baseline | Extended |
|---|---|---|
| Soundness | passed | passed |
| Source / sink places | 1 / 1 | 1 / 1 |
| Unbounded places | 0 | 0 |
| Dead transitions | 0 | 0 |
| Non-live transitions | 0 | 0 |
| Free-choice violation groups | 1 | 3 |
| PT-handles / TP-handles | 16 / 15 | 40 / 24 |
The role nets on their own are free-choice and well-structured. Composing them adds structural dependencies: the integrated systems are sound but not free-choice and not fully well-structured. Telling these two kinds of property apart, what the model guarantees and what its shape looks like, is the point of the analysis.
From requirements to proofs.
The two BPMN models and all eight Petri nets are on GitHub in editable form, with the report that connects the business scenario to the formal analysis.