@article{35a9f6b460dc41598e84b29e813fe398,
title = "Global and local deadlock freedom in BIP",
abstract = "We present a criterion for checking local and global deadlock freedom of finite state systems expressed in BIP: A component-based framework for constructing complex distributed systems. Our criterion is evaluated by model-checking a set of subsystems of the overall large system. If satisfied in small subsystems, it implies deadlock-freedom of the overall system. If not satisfied, then we re-evaluate over larger subsystems, which improves the accuracy of the check. When the subsystem being checked becomes the entire system, our criterion becomes complete for deadlock-freedom. Hence our criterion only fails to decide deadlock freedom because of computational limitations: state-space explosion sets in when the subsystems become too large. Our method thus combines the possibility of fast response together with theoretical completeness. Other criteria for deadlock freedom, in contrast, are incomplete in principle, and so may fail to decide deadlock freedom even if unlimited computational resources are available. Also, our criterion certifies freedom from local deadlock, in which a subsystem is deadlocked while the rest of the system executes. Other criteria only certify freedom from global deadlock.We present experimental results for dining philosophers and for a multi-Token-based resource allocation system,which subsumes several data arbiters and schedulers, including Milner's token-based scheduler.",
keywords = "Alternation, Completeness, Nondeterminism",
author = "Attie, {Paul C.} and Saddek Bensalem and Marius Bozga and Mohamad Jaber and Joseph Sifakis and Zaraket, {Fadi A.}",
note = "Funding Information: The research leading to these results has received funding from University Research Board (URB) at the American University of Beirut. Authors{\textquoteright} addresses: P. C. Attie, American University of Beirut, PO Box 11-0236, Riad El Solh, Beirut, 1107 2020, Lebanon; email: paul.attie@aub.edu.lb; S. Bensalem, UJF-Grenoble 1/CNRS VERIMAG, UMR 5104, Grenoble, F-38041, France, Sad-dek; email: Bensalem@imag.fr; M. Bozga, UJF-Grenoble 1/CNRS VERIMAG, UMR 5104, Grenoble, F-38041, France, Marius; email: Bozga@imag.fr; M. Jaber, American University of Beirut, PO Box 11-0236, Riad El Solh, Beirut, 1107 2020, Lebanon; email: mj54@aub.edu.lb; J. Sifakis, Ecole Polytechnique Federale Lausanne, Route Cantonale, Lausanne, 1015, Switzerland; email: joseph.sifakis@imag.fr; F. A. Zaraket, American University of Beirut, PO Box 11-0236, Riad El Solh, Beirut, 1107 2020, Lebanon; email: fz11@aub.edu.lb. Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org. {\textcopyright} 2018 ACM 1049-331X/2018/01-ART9 $15.00 https://doi.org/10.1145/3152910",
year = "2018",
month = jan,
doi = "10.1145/3152910",
language = "English (US)",
volume = "26",
journal = "ACM Transactions on Software Engineering and Methodology",
issn = "1049-331X",
publisher = "Association for Computing Machinery (ACM)",
number = "3",
}