An abstract framework for deadlock prevention in BIP

Paul C. Attie, Saddek Bensalem, Marius Bozga, Mohamad Jaber, Joseph Sifakis, Fadi A. Zaraket

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Scopus citations

Abstract

We present a sound but incomplete criterion for checking deadlock freedom of finite state systems expressed in BIP: a component-based framework for the construction of complex distributed systems. Since deciding deadlock-freedom for finite-state concurrent systems is PSPACE-complete, our criterion gives up completeness in return for tractability of evaluation. Our criterion can be evaluated by model-checking subsystems of the overall large system. The size of these subsystems depends only on the local topology of direct interaction between components, and not on the number of components in the overall system. We present two experiments, in which our method compares favorably with existing approaches. For example, in verifying deadlock freedom of dining philosphers, our method shows linear increase in computation time with the number of philosophers, whereas other methods (even those that use abstraction) show super-linear increase, due to state-explosion.

Original languageEnglish (US)
Title of host publicationFormal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on DisCoTec 2013, Proceedings
Pages161-177
Number of pages17
DOIs
StatePublished - 2013
EventJoint IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013 - Florence, Italy
Duration: Jun 3 2013Jun 5 2013

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7892 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

ConferenceJoint IFIP WG 6.1 International Conference on Formal Techniques for Distributed Systems, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on Distributed Computing Techniques, DisCoTec 2013
CountryItaly
CityFlorence
Period6/3/136/5/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'An abstract framework for deadlock prevention in BIP'. Together they form a unique fingerprint.

  • Cite this

    Attie, P. C., Bensalem, S., Bozga, M., Jaber, M., Sifakis, J., & Zaraket, F. A. (2013). An abstract framework for deadlock prevention in BIP. In Formal Techniques for Distributed Systems - Joint IFIP WG 6.1 International Conference, FMOODS/FORTE 2013, Held as Part of the 8th International Federated Conference on DisCoTec 2013, Proceedings (pp. 161-177). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7892 LNCS). https://doi.org/10.1007/978-3-642-38592-6_12