First-Order Dynamic Logic for Compensable Processes

Abstract : Compensable programs offer a convenient paradigm to deal with long-running transactions, because they offer a structured and modular approach to the composition of distributed transactional activities, like services. The basic idea is that each activity has its own compensation and that the compensable program fixes the order of execution of such activities. The main problem is how to guarantee that if one or even many faults occur then the compensations are properly executed so to reach a consistent configuration of the system. We propose a formal model for such problems based on a concurrent extension of dynamic logic that allows us to distill the hypothesis under which the correctness of compensable programs can be ensured. The main result establishes that if basic activities have a correct compensation we can show the correctness of any compound compensable program. Moreover, we can use dynamic logic to reason about behavioural and transactional properties of programs.
Type de document :
Communication dans un congrès
Marjan Sirjani. 14th International Conference on Coordination Models and Languages (COORDINATION), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7274, pp.104-121, 2012, Coordination Models and Languages. 〈10.1007/978-3-642-30829-1_8〉
Liste complète des métadonnées

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

https://hal.inria.fr/hal-01529601
Contributeur : Hal Ifip <>
Soumis le : mercredi 31 mai 2017 - 10:00:04
Dernière modification le : mercredi 31 mai 2017 - 10:00:57
Document(s) archivé(s) le : mercredi 6 septembre 2017 - 15:05:59

Fichier

978-3-642-30829-1_8_Chapter.pd...
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité 4.0 International License

Identifiants

Citation

Roberto Bruni, Carla Ferreira, Anne Kersten Kauer. First-Order Dynamic Logic for Compensable Processes. Marjan Sirjani. 14th International Conference on Coordination Models and Languages (COORDINATION), Jun 2012, Stockholm, Sweden. Springer, Lecture Notes in Computer Science, LNCS-7274, pp.104-121, 2012, Coordination Models and Languages. 〈10.1007/978-3-642-30829-1_8〉. 〈hal-01529601〉

Partager

Métriques

Consultations de la notice

58

Téléchargements de fichiers

19