Consistently Formalizing a Business Process and its Properties for Verification: A Case Study

Abstract : Formal verification of business process models can be done through model checking (also known as property checking), where a model checker tool may automatically find violations of properties in a process model. This approach obviously has formal representations as a prerequisite. However, a key challenge for applying this approach in practice is to consistently formalize the process and its properties, which clearly cannot be done automatically. We studied this challenge in a case study of formally verifying an informally given business process against a guideline written like a legal text. Major lessons learned from this case study are that formalizing is key to success and that in its course a semi-formal representation of properties is useful. In the course of such a step-wise and incremental formalization, problems with the given process model have been found already, apart from those found with a model checker tool that used the formal property specification. In total, our approach revealed five problems not found by the official review. In summary, this paper investigates in a case study consistently formalizing a business process and its properties for verification through model checking.
Type de document :
Communication dans un congrès
Jolita Ralyté; Sergio España; Óscar Pastor. 8th Practice of Enterprise Modelling (P0EM), Nov 2015, Valencia, Spain. Springer, Lecture Notes in Business Information Processing, LNBIP-235, pp.126-140, 2015, The Practice of Enterprise Modeling. 〈10.1007/978-3-319-25897-3_9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01442302
Contributeur : Hal Ifip <>
Soumis le : vendredi 20 janvier 2017 - 15:21:51
Dernière modification le : vendredi 20 janvier 2017 - 15:25:47
Document(s) archivé(s) le : vendredi 21 avril 2017 - 15:41:11

Fichier

978-3-319-25897-3_9_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Michael Rathmair, Ralph Hoch, Hermann Kaindl, Roman Popp. Consistently Formalizing a Business Process and its Properties for Verification: A Case Study. Jolita Ralyté; Sergio España; Óscar Pastor. 8th Practice of Enterprise Modelling (P0EM), Nov 2015, Valencia, Spain. Springer, Lecture Notes in Business Information Processing, LNBIP-235, pp.126-140, 2015, The Practice of Enterprise Modeling. 〈10.1007/978-3-319-25897-3_9〉. 〈hal-01442302〉

Partager

Métriques

Consultations de la notice

29

Téléchargements de fichiers

37