Verifiable UML Artifact-Centric Business Process Models (Extended Version)
Diego Calvanese, Marco Montali, Montserrat Estanol, Ernest, Teniente

TL;DR
This paper integrates artifact-centric business process modeling with formal verification techniques using UML, enabling the verification of complex temporal properties in business models.
Contribution
It merges modeling and verification research, applying recent decidability results to UML-based artifact models for enhanced verifiability.
Findings
Verification of UML artifact models against rich temporal properties is feasible.
Methodology steps ensure decidability in significant cases.
Results are adaptable to various artifact lifecycle languages.
Abstract
Artifact-centric business process models have gained increasing momentum recently due to their ability to combine structural (i.e., data related) with dynamical (i.e., process related) aspects. In particular, two main lines of research have been pursued so far: one tailored to business artefact modeling languages and methodologies, the other focused on the foundations for their formal verification. In this paper, we merge these two lines of research, by showing how recent theoretical decidability results for verification can be fruitfully transferred to a concrete UML-based modeling methodology. In particular, we identify additional steps in the methodology that, in significant cases, guarantee the possibility of verifying the resulting models against rich first-order temporal properties. Notably, our results can be seamlessly transferred to different languages for the specification of…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
