Skip to main content
SpringerLink
Log in
Book cover

Engineering Distributed Objects pp 116–128Cite as

Using Model Checking to Detect Deadlocks in Distributed Object Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1999))

Abstract

We demonstrate how the use of synchronization primitives and threading policies in distributed object middleware can lead to dead- locks. We identify that object middleware only has a few built-in syn- chronization and threading primitives. We suggest to express them as stereotypes in UML models to allow designers to model synchronization and threading of distributed object systems at appropriate levels of ab- straction. We define the semantics of these stereotypes by a mapping to a process algebra. This allows us to use model checking techniques that are available for process algebras to detect the presence or absence of deadlocks. We also discuss how the results of these model checks can be related back to the UML diagrams.

This paper is an extended version of [6]

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R. Allen and D. Garlan. A Formal Basis for Architectural Connection. ACM Transactions on Software Engineering and Methodology, 6(3):213–249, June 1997. 127

    Article  Google Scholar 

  2. S.-C. Cheung and J. Kramer. Checking Safety Properties Using Compositional Reachability Analysis. ACM Transactions on Software Engineering and Methodology, 8(1):49–7, 1999. 126

    Article  Google Scholar 

  3. R. Cleaveland, J. Parrow, and B Steffen. The Concurrency Workbench: A Semantics Based Tool for the Verification of Concurrent Systems. ACM Transactions on Programming Languages and Systems, 15(1):36–72, 1993. 127

    Article  Google Scholar 

  4. E. di Nitto and D. Rosenblum. Exploiting ADLs to Specify Architectural Styles Induced by Middleware Infrastructures. In Proc. of the 21st Int. Conf. on Software Engineering, Los Angeles, California, pages 13–22. ACM Press, 1999. 127

    Google Scholar 

  5. W. Emmerich. Engineering Distributed Objects. John Wiley & Sons, Apr. 2000.116, 117

    Google Scholar 

  6. W. Emmerich and N. Kaveh. Model Checking Distributed Objects. In B. Balzer and H. Obbink, editors, Proc. of the 4th International Software Architecture Workshop, Limerick, Ireland, 2000. To appear. 116

    Google Scholar 

  7. M. Gaspari and G. Zavattaro. A Process Algebraic Specification of the New Asynchronous CORBA Messaging Service. In Proceedings of the 13th European Conference on Object-Oriented Programming, ECOOP’99, volume 1628 of Lecture Notes in Computer Science, pages 495–518. Springer, 1999. 127

    Google Scholar 

  8. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985. 126

    Google Scholar 

  9. J. Magee and J. Kramer. Concurrency: Models and Programs-From Finite State Models to Java Programs. John Wiley, 1999. 118, 122, 126

    Google Scholar 

  10. R. Milner. Communication and Concurrency. Prentice-Hall, 1995. 126

    Google Scholar 

  11. R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge University Press, 1999. 126

    Google Scholar 

  12. C. Nentwich, W. Emmerich, A. Finkelstein, and A. Zisman. Browsing Objects in XML. Research Note RN/99/41, University College London, Dept. of Computer Science, 1999. 126

    Google Scholar 

  13. Object Management Group. The Common Object Request Broker: Architecture and Specification Revision 2.0. 492 Old Connecticut Path, Framingham, MA 01701, USA, July 1995. 122

    Google Scholar 

  14. Object Management Group. XML Meta Data Interchange (XMI)-Proposal to the OMG OA&DTF RFP 3: Stream-based Model Interchange Format (SMIF). 492 Old Connecticut Path, Framingham, MA 01701, USA, Oct. 1998. 126

    Google Scholar 

  15. M. Shaw and D. Garlan. Software Architecture: Perspectives on an Emerging Discipline. Prentice Hall, 1996. 127

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, University College London, WC1E 6BT, London, UK

    Nima Kaveh

Authors
  1. Nima Kaveh
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University College London, Gower Street, London, WC1E 6BT, UK

    Wolfgang Emmerich

  2. IBM T.J. Watson Research Center, 30 Saw Mill River Road Hawthorne, NY, 10532, USA

    Stefan Tai

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kaveh, N. (2001). Using Model Checking to Detect Deadlocks in Distributed Object Systems. In: Emmerich, W., Tai, S. (eds) Engineering Distributed Objects. Lecture Notes in Computer Science, vol 1999. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45254-0_11

Download citation

  • DOI: https://doi.org/10.1007/3-540-45254-0_11

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-41792-7

  • Online ISBN: 978-3-540-45254-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation