Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs

Abstract : The Symbolic Observation Graph (SOG) associated with a labelled transition system and a subset of its labels is an efficient BDD-based abstraction representing the behavior of a system. The goal of this paper is to compose SOGs such that the resulting SOG is still small but represents the behavior of the composed business process in an appropriate way. In particular, we would like to deduce the properties of a composed business process by analysing the composition of the SOGs associated with its components. This question was already answered for the deadlock-freeness property in previous work. In this paper, we extend this result to other generic properties: the so-called soundness properties. These properties guarantee the absence of livelocks, deadlocks and other anomalies that can be formulated without domain knowledge. Thus, we show how the SOG can be adapted and used so that the verification of several variants of the soundness property can be performed modularly.
Type de document :
Communication dans un congrès
Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.67-83, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_5〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01528733
Contributeur : Hal Ifip <>
Soumis le : lundi 29 mai 2017 - 15:53:58
Dernière modification le : jeudi 11 janvier 2018 - 06:17:32
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 11:29:59

Fichier

978-3-642-30793-5_5_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Kais Klai, Jörg Desel. Checking Soundness of Business Processes Compositionally Using Symbolic Observation Graphs. Holger Giese; Grigore Rosu. 14th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS) / 32nd International Conference on Formal Techniques for Networked and Distributed Systems (FORTE), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7273, pp.67-83, 2012, Formal Techniques for Distributed Systems. 〈10.1007/978-3-642-30793-5_5〉. 〈hal-01528733〉

Partager

Métriques

Consultations de la notice

67

Téléchargements de fichiers

29