Skip to main content
SpringerLink
Log in

Specifying Properties of Dynamic Architectures Using Configuration Traces

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2016 (ICTAC 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9965))

Included in the following conference series:

Abstract

The architecture of a system describes the system’s overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures became increasingly important. In such architectures, components may appear or disappear, and connections may change over time.

Despite the growing importance of dynamic architectures, the specification of properties for those architectures remains a challenge. To address this problem, we introduce the notion of configuration traces to model properties of dynamic architectures. Then, we investigate these properties to identify different types thereof. We show completeness and consistency of these types, i.e., we show that (almost) every property can be separated into these types and that a property of one type does not impact properties of other types.

Configuration traces can be used to specify general properties of dynamic architectures and the separation into different types provides a systematic way for their specification. To evaluate our approach we apply it to the specification and verification of the Blackboard pattern in Isabelle/HOL.

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

Notes

  1. 1.

    We use \(\Vert c \Vert \) to denote that component c is active at the corresponding time.

  2. 2.

    The script can be downloaded at http://www.marmsoler.com/pattern/Blackboard.thy

References

  1. Abowd, G.D., Allen, R., Garlan, D.: Formalizing style to understand descriptions of software architecture. ACM TOSEM 4, 319–364 (1995)

    Article  Google Scholar 

  2. Allen, R., Douence, R., Garlan, D.: Specifying and analyzing dynamic software architectures. In: Astesiano, E. (ed.) FASE 1998. LNCS, vol. 1382, pp. 21–37. Springer, Heidelberg (1998). doi:10.1007/BFb0053581

    Chapter  Google Scholar 

  3. Allen, R.J.: A formal approach to software architecture. Technical report, DTIC Document (1997)

    Google Scholar 

  4. Bernardo, M., Ciancarini, P., Donatiello, L.: On the formalization of architectural types with process algebras. ACM SIGSOFT SEN 25, 140–148 (2000)

    Article  Google Scholar 

  5. Bradbury, J.S., Cordy, J.R., Dingel, J., Wermelinger, M.: A survey of self-management in dynamic software architecture specifications. In: WOSS (2004)

    Google Scholar 

  6. Broy, M.: A logical basis for component-oriented software and systems engineering. Comput. J. 53(10), 1758–1782 (2010)

    Article  Google Scholar 

  7. Broy, M.: A model of dynamic systems. In: Bensalem, S., Lakhneck, Y., Legay, A. (eds.) ETAPS 2014. LNCS, vol. 8415, pp. 39–53. Springer, Heidelberg (2014). doi:10.1007/978-3-642-54848-2_3

    Google Scholar 

  8. Buschmann, F., Meunier, R., Rohnert, H., Sommerlad, P., Stal, M.: A system of patterns: Pattern-oriented software architecture (1996)

    Google Scholar 

  9. Castro, P.F., Aguirre, N.M., López Pombo, C.G., Maibaum, T.S.E.: Towards managing dynamic reconfiguration of software systems in a categorical setting. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 306–321. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14808-8_21

    Chapter  Google Scholar 

  10. Clements, P.C.: A survey of architecture description languages. In: IWSSD (1996)

    Google Scholar 

  11. Dashofy, E.M., Van der Hoek, A., Taylor, R.N.: A highly-extensible, xml-based architecture description language. In: WICSA, IEEE (2001)

    Google Scholar 

  12. Fiadeiro, J.L., Lopes, A.: A model for dynamic reconfiguration in service-oriented architectures. Softw. Syst. Model. 12(2), 349–367 (2013)

    Article  Google Scholar 

  13. Garlan, D.: Formal modeling and analysis of software architecture: components, connectors, and events. In: Bernardo, M., Inverardi, P. (eds.) SFM 2003. LNCS, vol. 2804, pp. 1–24. Springer, Heidelberg (2003). doi:10.1007/978-3-540-39800-4_1

    Chapter  Google Scholar 

  14. Hirsch, D., Montanari, U.: Two graph-based techniques for software architecture reconfiguration. Electron. Notes Theor. Comput. Sci. 51, 177–190 (2002)

    Article  MATH  Google Scholar 

  15. Inverardi, P., Wolf, A.L.: Formal specification and analysis of software architectures using the chemical abstract machine model. IEEE TSE 21, 373–386 (1995)

    Google Scholar 

  16. Le Métayer, D.: Describing software architecture styles using graph grammars. IEEE TSE 24, 521–533 (1998)

    Google Scholar 

  17. Luckham, D.C., Kenney, J.J., Augustin, L.M., Vera, J., Bryan, D., Mann, W.: Specification and analysis of system architecture using Rapide. IEEE TSE 21, 336–355 (1995)

    Google Scholar 

  18. Magee, J., Kramer, J.: Dynamic structure in software architectures. ACM SIGSOFT SEN 21, 3–14 (1996)

    Article  Google Scholar 

  19. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New york (2012)

    MATH  Google Scholar 

  20. Medvidovic, N.: ADLs and dynamic architecture changes. In: ISAW (1996)

    Google Scholar 

  21. Moriconi, M., Qian, X., Riemenschneider, R.A.: Correct architecture refinement. IEEE TSE 21, 356–372 (1995)

    Google Scholar 

  22. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer Science & Business Media, Heidelberg (2002)

    Book  MATH  Google Scholar 

  23. Oquendo, F.: \(\pi \)-ADL: an architecture description language based on the higher-order typed \(\pi \)-calculus for specifying dynamic and mobile software architectures. ACM SIGSOFT SEN 29, 1–14 (2004)

    Google Scholar 

  24. Penix, J., Alexander, P., Havelund, K.: Declarative specification of software architectures. In: ASE (1997)

    Google Scholar 

  25. Shaw, M., Garlan, D.: Software Architecture: Perspectives on an Emerging Discipline, vol. 1. Prentice Hall Englewood Cliffs, Upper Saddle River (1996)

    MATH  Google Scholar 

  26. Spivey, J.M., Abrial, J.: The Z notation (1992)

    Google Scholar 

  27. Taylor, R.N., Medvidovic, N., Dashofy, E.M.: Software Architecture: Foundations, Theory, and Practice. Wiley Publishing, Hoboken (2009)

    Book  Google Scholar 

  28. Wenzel, M.: Isabelle/Isar: a generic framework for human-readable proof documents. From Insight to Proof: Festschrift in Honour of Andrzej Trybulec 10, 277–298 (2007)

    Google Scholar 

  29. Wermelinger, M., Lopes, A., Fiadeiro, J.L.: A graph based architectural (re) configuration language. ACM SIGSOFT SEN 26(5), 21–32 (2001)

    Article  Google Scholar 

  30. Wirsing, M.: Algebraic Specification. MIT Press, Cambridge (1991)

    MATH  Google Scholar 

Download references

Acknowledgments

We would like to thank Jonas Eckhardt, Vasileios Koutsoumpas, and the reviewers of ICTAC 2016 for their comments and helpful suggestions.

Author information

Authors and Affiliations

  1. Technische Universität München, Munich, Germany

    Diego Marmsoler & Mario Gleirscher

Authors
  1. Diego Marmsoler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mario Gleirscher
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Diego Marmsoler .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco Centro de Informática, Recife, Pernambuco, Brazil

    Augusto Sampaio

  2. Deptartment of Electrical Engineering BL, National Taiwan University, Taipei, Taiwan

    Farn Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Marmsoler, D., Gleirscher, M. (2016). Specifying Properties of Dynamic Architectures Using Configuration Traces. In: Sampaio, A., Wang, F. (eds) Theoretical Aspects of Computing – ICTAC 2016. ICTAC 2016. Lecture Notes in Computer Science(), vol 9965. Springer, Cham. https://doi.org/10.1007/978-3-319-46750-4_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46750-4_14

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46749-8

  • Online ISBN: 978-3-319-46750-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation