Verifying Timed BPMN Processes Using Maude

Francisco Durán 1 Gwen Salaün 2
2 CONVECS - Construction of verified concurrent systems
Inria Grenoble - Rhône-Alpes, LIG - Laboratoire d'Informatique de Grenoble
Abstract : A business process is a collection of structured activities producing a particular product or software. BPMN is a workflow-based graphical notation for specifying business processes. Formally analyzing such processes is a crucial challenge in order to avoid erroneous executions of the corresponding software. In this paper, we focus on timed business processes where execution time can be associated to several BPMN constructs. We propose an encoding of timed business processes into the Maude language, which allows one to automatically verify several properties of interest on processes such as the maximum/minimum/av-erage execution time or the timed degree of parallelism that provides a valuable guide for the problem of resource allocation. The analysis is achieved using the rewriting-based tools available in Maude, which also provides other techniques (e.g., reachability analysis and model checking) for verifying BPMN specifications. We applied our approach on a large set of BPMN processes for evaluation purposes.
Type de document :
Communication dans un congrès
Jean-Marie Jacquet; Mieke Massink. 19th International Conference on Coordination Languages and Models (COORDINATION), Jun 2017, Neuchâtel, Switzerland. Springer, Lecture Notes in Computer Science, LNCS-10319, pp.219-236, 2017, Coordination Models and Languages. 〈http://2017.discotec.org〉. 〈10.1007/978-3-319-59746-1_12〉
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01538104
Contributeur : Gwen Salaün <>
Soumis le : mardi 13 juin 2017 - 11:49:10
Dernière modification le : jeudi 11 janvier 2018 - 06:23:43
Document(s) archivé(s) le : mardi 12 décembre 2017 - 15:01:18

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Francisco Durán, Gwen Salaün. Verifying Timed BPMN Processes Using Maude. Jean-Marie Jacquet; Mieke Massink. 19th International Conference on Coordination Languages and Models (COORDINATION), Jun 2017, Neuchâtel, Switzerland. Springer, Lecture Notes in Computer Science, LNCS-10319, pp.219-236, 2017, Coordination Models and Languages. 〈http://2017.discotec.org〉. 〈10.1007/978-3-319-59746-1_12〉. 〈hal-01538104〉

Partager

Métriques

Consultations de la notice

167

Téléchargements de fichiers

82