A Petri Net Based Analysis of Deadlocks for Active Objects and Futures

Abstract : We give two different notions of deadlock for systems based on active objects and futures. One is based on blocked objects and conforms with the classical definition of deadlock by Coffman, Jr. et al. The other one is an extended notion of deadlock based on blocked processes which is more general than the classical one. We introduce a technique to prove deadlock freedom of systems of active objects. To check deadlock freedom an abstract version of the program is translated into Petri nets. Extended deadlocks, and then also classical deadlock, can be detected via checking reachability of a distinct marking. Absence of deadlocks in the Petri net constitutes deadlock freedom of the concrete system.
Type de document :
Communication dans un congrès
Corina S. Pasareanu and Gwen Salaün. Formal Aspects of Component Software, 9th International Symposium, FACS 2012, 2012, Mountain View, United States. Springer, 7684, pp.110-127, 2013, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/hal-00909292
Contributeur : Davide Sangiogi <>
Soumis le : mardi 26 novembre 2013 - 10:44:39
Dernière modification le : jeudi 11 janvier 2018 - 17:01:01

Identifiants

  • HAL Id : hal-00909292, version 1

Collections

Citation

Frank S. Boer, Mario Bravetti, Immo Grabe, Matias David Lee, Martin Steffen, et al.. A Petri Net Based Analysis of Deadlocks for Active Objects and Futures. Corina S. Pasareanu and Gwen Salaün. Formal Aspects of Component Software, 9th International Symposium, FACS 2012, 2012, Mountain View, United States. Springer, 7684, pp.110-127, 2013, Lecture Notes in Computer Science. 〈hal-00909292〉

Partager

Métriques

Consultations de la notice

114