Skip to main content
SpringerLink
Log in

Model Checking for Software Architectures

  • Conference paper
Software Architecture (EWSA 2004)

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

Included in the following conference series:

Abstract

Software architectures are engineering artifacts which provide high-level descriptions of complex systems. Certain recent architecture description languages (Asls) allow to represent a system’s structure and behaviour together with its dynamic changes and evolutions. Model checking techniques offer a useful way for automatically verifying finite-state Adl descriptions w.r.t. their desired correctness requirements. In this position paper, we discuss several issues related to the application of model checking in the area of software architectures, underlining the aspects of interest for current and future research (construction of state spaces, expression and verification of requirements, state explosion).

This study was supported by the European Ist-2001-32360 project “ArchWare”.

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abate, P., Bernardo, M.: A Scalable Approach to the Design of SW Architectures with Dynamically Created/Destroyed Components. In: Proc. of SEKE 2002, July 2002, pp. 255–262. ACM, New York (2002)

    Chapter  Google Scholar 

  2. Allen, R.J.: A Formal Approach to Software Architecture. Ph.D. Thesis, Technical Report CMU-CS-97-144, Carnegie Mellon University (May 1997)

    Google Scholar 

  3. Allen, R.J., Douence, R., Garlan, D.: Specifying and Analyzing Dynamic Software Architectures. In: Astesiano, E. (ed.) ETAPS 1998 and FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  4. Bernardo, M., Ciancarini, P., Donatiello, L.: Detecting Architectural Mismatches in Process Algebraic Descriptions of Software Systems. In: Proc. of WICSA 2001, August 2001, pp. 77–86. IEEE Computer Society, Los Alamitos (2001)

    Google Scholar 

  5. Chaudet, C., Oquendo, F.: Pi-SPACE: A Formal Architecture Description Language Based on Process Algebra for Evolving Software Systems. In: Proc. of ASE 2000, September 2000, pp. 245–248 (2000)

    Google Scholar 

  6. Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  7. Garavel, H.: OPEN/CÆSAR: An Open Software Architecture for Verification, Simulation, and Testing. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 68–84. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  8. Garavel, H., Lang, F.: SVL: a Scripting Language for Compositional Verification. In: Proc. of FORTE 2001, August 2001, pp. 377–392. IFIP, Kluwer Academic Publishers (2001)

    Google Scholar 

  9. Garavel, H., Lang, F., Mateescu, R.: An Overview of CADP 2001. EASST Newsletter 4, 13–24 (2002)

    Google Scholar 

  10. Garavel, H., Sifakis, J.: Compilation and Verification of LOTOS Specifications. In: Proc. of PSTV 1990, June 1990, pp. 379–394. IFIP (1990)

    Google Scholar 

  11. Garavel, H., Sighireanu, M.: Towards a Second Generation of Formal Description Techniques – Rationale for the Design of E-LOTOS. In: Proc. of FMICS 1998, May 1998, pp. 187–230. CWI (1998)

    Google Scholar 

  12. Garlan, D., Khersonsky, S., Kim, J.S.: Model Checking Publish-Subscribe Systems. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 166–180. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  13. Groote, J.F.: A Note on n Similar Parallel Processes. In: Proc. of FMICS 1997, July 1997, pp. 65–75. CNR (1997)

    Google Scholar 

  14. ISO/IEC. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. ISO Standard 8807 (1989)

    Google Scholar 

  15. ISO/IEC. Enhancements to LOTOS (E-LOTOS). ISO Standard 15437:2001

    Google Scholar 

  16. Kramer, J., Magee, J., Uchitel, S.: Software Architecture Modeling & Analysis: A Rigorous Approach. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 44–51. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  17. 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)

    Google Scholar 

  18. Mateescu, R.: Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 281–295. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  19. Mateescu, R., Sighireanu, M.: Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Sci. of Comp. Prog. 46(3), 255–281 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  20. Medvidovic, N., Taylor, R.N.: A Classification and Comparison Framework for Software Architecture Description Languages. IEEE Transactions on Software Engineering 26(1), 70–93 (2000)

    Article  Google Scholar 

  21. Milner, R.: Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, Cambridge (1999)

    MATH  Google Scholar 

  22. Oquendo, F., Alloui, I., Cîmpan, S., Verjus, H.: The ArchWare ADL: Definition of the Abstract Syntax and Formal Semantics. Project Deliverable D1.1b, European project IST 2001-32360 “ArchWare” (December 2002)

    Google Scholar 

  23. Pace, G., Lang, F., Mateescu, R.: Calculating τ-Confluence Compositionally. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 446–459. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  24. Peled, D.A., Pratt, V.R., Holzmann, G.J. (eds.): Partial Order Methods in Verification. DIMACS series, vol. 29. American Mathematical Society, Providence (1997)

    MATH  Google Scholar 

  25. Roscoe, A.W.: Model-Checking CSP. In: A Classical Mind, Essays in Honour of C.A.R. Hoare, Prentice-Hall, Englewood Cliffs (1994)

    Google Scholar 

  26. Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)

    MATH  Google Scholar 

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

    Google Scholar 

  28. Stirling, C.: Modal and Temporal Properties of Processes. Springer, Heidelberg (2001)

    Google Scholar 

  29. Victor, B., Moller, F.: The Mobility Workbench – A Tool for the π-Calculus. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 428–440. Springer, Heidelberg (1994)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inria Rhône-Alpes / Vasy, 655, avenue de l’Europe, F-38330, Montbonnot Saint Martin, France

    Radu Mateescu

Authors
  1. Radu Mateescu
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. VALORIA Laboratory, University of South Brittany, Tohannic Campus, 56017, Vannes, France

    Flavio Oquendo

  2. University of Manchester, M13 9PL, Manchester, UK

    Brian C. Warboys

  3. School of Computer Science, University of St Andrews, North Haugh, KY16 9SX, St Andrews Fife, UK

    Ron Morrison

Rights and permissions

Reprints and permissions

Copyright information

© 2004 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mateescu, R. (2004). Model Checking for Software Architectures. In: Oquendo, F., Warboys, B.C., Morrison, R. (eds) Software Architecture. EWSA 2004. Lecture Notes in Computer Science, vol 3047. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24769-2_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-24769-2_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-22000-8

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation