TY - GEN
T1 - An abstract framework for deadlock prevention in BIP
AU - Attie, Paul C.
AU - Bensalem, Saddek
AU - Bozga, Marius
AU - Jaber, Mohamad
AU - Sifakis, Joseph
AU - Zaraket, Fadi A.
N1 - Funding Information:
The research leading to these results has received funding from the European Community’s Seventh Framework Programme [FP7/2007-2013] under grant agreement no. 288175 (CERTAINTY) and no 257414 (ASCENS).
PY - 2013
Y1 - 2013
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84885011474&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84885011474&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-38592-6_12
DO - 10.1007/978-3-642-38592-6_12
M3 - Conference contribution
AN - SCOPUS:84885011474
SN - 9783642385919
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 161
EP - 177
BT - 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
T2 - Joint 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
Y2 - 3 June 2013 through 5 June 2013
ER -