%0 Conference Proceedings
%T An Abstract Framework for Deadlock Prevention in BIP
%+ Department of Computer Science
%+ VERIMAG (VERIMAG - IMAG)
%+ Rigorous System Design Laboratory [Lausanne] (RISD)
%A Attie, Paul C.
%A Bensalem, Saddek
%A Bozga, Marius
%A Jaber, Mohamad
%A Sifakis, Joseph
%A Zaraket, Fadi A.
%Z Part 6: Session 5: Model Checking
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 15th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOOODS) / 33th International Conference on Formal Techniques for Networked and Distributed Systems (FORTE)
%C Florence, Italy
%Y Dirk Beyer
%Y Michele Boreale
%I Springer
%3 Formal Techniques for Distributed Systems
%V LNCS-7892
%P 161-177
%8 2013-06-03
%D 2013
%R 10.1007/978-3-642-38592-6_12
%Z Computer Science [cs]/Embedded SystemsConference papers
%X 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.
%G English
%Z TC 6
%Z WG 6.1
%2 https://hal.science/hal-00878752/document
%2 https://hal.science/hal-00878752/file/978-3-642-38592-6_12_Chapter.pdf
%L hal-00878752
%U https://hal.science/hal-00878752
%~ UGA
%~ IMAG
%~ CNRS
%~ UNIV-GRENOBLE1
%~ INPG
%~ LORIA2
%~ VERIMAG
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-FORTE
%~ IFIP-DISCOTEC
%~ IFIP-LNCS-7892
%~ IFIP-FMOODS