Abstract
To alleviate the state explosion problem in deadlock detection for parallel composition of components, we extend the classical labeled transition system models to make both abstraction and compositional reasoning applicable, and then propose a compositional abstraction refinement approach to deadlock detection. The abstraction of a component is defined by means of a quotient on states with respect to some equivalence relation, and the abstraction model for the component composition can be built by composing the abstractions of components without constructing the complete state space of the concrete component composition. Theorems for abstraction refinement of deadlock detection are proposed and proved. Validating an abstract deadlock and refining the abstraction are all carried out component-wise.
This work is supported by National Natural Science Foundation of China (NSFC) under grant No. 60970007, the Natural Science Foundation of Shanghai Municipality of China under Grant No.09ZR1412100, Science and Technology Commission of Shanghai Municipality under Grant No. 10510704900, and Shanghai Leading Academic Discipline Project, Project Number: J50103.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 154–169. Springer, Heidelberg (2000)
Ball, T., Majumdar, R., Millstein, T., Rajamani, S.K.: Automatic predicate abstraction of C programs. ACM SIGPLAN Notices 36(5), 203–213 (2001)
Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)
Henzinger, T.A., Qadeer, S., Rajamani, S.K.: Decomposing refinement proofs using assume-guarantee reasoning. In: Proceedings of the 2000 International Conference on Computer-Aided Design (ICCAD 2000), pp. 245–252. IEEE Computer Society Press, Los Alamitos (2000)
Cobleigh, J.M., Giannakopoulou, D., Păsăreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Chaki, S., Clarke, E., Ouaknine, J., Sharygina, N.: Automated, Compositional and Iterative Deadlock Detection. In: Proceedings of the Second ACM-IEEE International Conference on Formal Methods and models for Codesign (MEMOCODE), pp. 201–210. IEEE Press, Los Alamitos (2004)
Corbett, J.C.: Evaluating deadlock detection methods for concurrent software. Software Engineering 22(3), 161–180 (1996)
Demartini, C., Iosif, R., Sisto, R.: A deadlock detection tool for concurrent java programs. Software: Practice & Experience 29(7), 577–603 (1999)
Awad, A., Puhlmann, F.: Structural Detection of Deadlocks in Business Process Models. In: Proceedings. of the 11th International Conference on Business Information Systems (BIS 2008). Lecture Notes in Business Information Processing, vol. 7, pp. 239–250 (2008)
Inverardi, P., Tivoli, M.: Deadlock-free software architectures for COM/DCOM applications. Journal of Systems & Software 65(3), 173–183 (2003)
Haque, W.: Concurrent deadlock detection in parallel programs. International Journal of Computers and Applications 28(1), 19–25 (2006)
Chaki, S., Clarke, E., Groce, A., Jha, S., Veith, H.: Modular verification of software components in C. IEEE Transactions on Software Engineering 30(6), 388–402 (2004)
Zeng, H.: Deadlock detection using abstraction refinement. Journal of Shanghai University 14(1), 1–5 (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Zeng, H., Miao, H. (2010). Deadlock Detection for Parallel Composition of Components. In: Lee, R. (eds) Computer and Information Science 2010. Studies in Computational Intelligence, vol 317. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15405-8_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-15405-8_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15404-1
Online ISBN: 978-3-642-15405-8
eBook Packages: EngineeringEngineering (R0)