Skip to main content
SpringerLink
Log in

A General Approach to Deadlock Freedom Verification for Software Architectures

  • Conference paper
  • First Online:
FME 2003: Formal Methods (FME 2003)

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

Included in the following conference series:

Abstract

When building complex software systems, the designer is faced with the problem of detecting mismatches arising from the activity of assembling components. The adoption of formal methods becomes unavoidable in order to support a precise identification of such mismatches in the early design stages. As far as deadlock freedom is concerned, some techniques appeared in the literature, which apply to formal specifications of software architectures under some constraints. In this paper we develop a novel technique for deadlock freedom verification that can be applied to arbitrary software architectures, thus overcoming the limitations of the previous techniques.

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

Access this chapter

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 84.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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

Institutional subscriptions

References

  1. Abowd, G.D., Allen, R., Garlan, D.: Formalizing Style to Understand Descriptions of Software Architecture. ACM Trans. on Software Engineering and Methodology 4, 319–364 (1995)

    Article  Google Scholar 

  2. Allen, R., Garlan, D.: A Formal Basis for Architectural Connection. ACM Trans. on Software Engineering and Methodology 6, 213–249 (1997)

    Article  Google Scholar 

  3. Bernardo, M., Ciancarini, P., Donatiello, L.: Architecting Families of Software Systems with Process Algebras. ACM Trans. on Software Engineering and Methodology 11, 386–426 (2002)

    Article  Google Scholar 

  4. Bernardo, M., Franzè, F.: Architectural Types Revisited: Extensible And/Or Connections. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 113–128. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Bernardo, M., Franzè, F.: Exogenous and Endogenous Extensions of Architectural Types. In: Arbab, F., Talcott, C. (eds.) COORDINATION 2002. LNCS, vol. 2315, pp. 40–55. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  6. Inverardi, P., Wolf, A.L.: Formal Specification and Analysis of Software Architectures Using the Chemical Abstract Machine Model. IEEE Trans. on Software Engineering 21, 373–386 (1995)

    Article  Google Scholar 

  7. Inverardi, P., Wolf, A.L., Yankelevich, D.: Static Checking of System Behaviors Using Derived Component Assumptions. ACM Trans. on Software Engineering and Methodology 9, 239–272 (2000)

    Article  Google Scholar 

  8. Magee, J., Dulay, N., Eisenbach, S., Kramer, J.: Specifying Distributed Software Architectures. In: Botella, P., Schäfer, W. (eds.) ESEC 1995. LNCS, vol. 989, pp. 137–153. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  9. Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)

    MATH  Google Scholar 

  10. Perry, D.E., Wolf, A.L.: Foundations for the Study of Software Architecture. ACM SIGSOFT Software Engineering Notes 17, 40–52 (1992)

    Article  Google Scholar 

  11. Shaw, M., Garlan, D.: Software Architecture: Perspectives on an Emerging Discipline. Prentice-Hall, Englewood Cliffs (1996)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Istituto di Scienze e Tecnologie dell’Informazione, Universitá di Urbino "Carlo Bo", Piazza della Repubblica 13, 61029, Urbino, Italy

    Alessandro Aldini & Marco Bernardo

Authors
  1. Alessandro Aldini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marco Bernardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science and Communication Engineering, Graduate School of Information Science and Electrical Engineering, Kyushu University, 6-10-1-Hakozaki, Higashi-ku, 812-8581, Fukuoka, Japan

    Keijiro Araki

  2. Istituto di Scienza e Tecnologie dell’Informazione “A. Faedo”, ISTI - CNR, Pisa, Italy

    Stefania Gnesi

  3. Dipartimento di Elettronica e Informazione, Politecnico di Milano, Italy

    Dino Mandrioli

Rights and permissions

Reprints and permissions

Copyright information

© 2003 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Aldini, A., Bernardo, M. (2003). A General Approach to Deadlock Freedom Verification for Software Architectures. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-45236-2_36

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-40828-4

  • Online ISBN: 978-3-540-45236-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation