Skip to main content
SpringerLink
Log in

APML: An Architecture Proof Modeling Language

  • Conference paper
  • First Online:
Formal Methods – The Next 30 Years (FM 2019)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 11800))

Included in the following conference series:

Abstract

To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.

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

References

  1. Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(03), 329–366 (2004)

    Article  MathSciNet  Google Scholar 

  2. Baier, C., Katoen, J., Larsen, K.: Principles of Model Checking. MIT Press (2008). https://books.google.de/books?id=nDQiAQAAIAAJ

  3. Ballarin, C.: Locales and locale expressions in Isabelle/Isar. In: Berardi, S., Coppo, M., Damiani, F. (eds.) TYPES 2003. LNCS, vol. 3085, pp. 34–50. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24849-1_3

    Chapter  MATH  Google Scholar 

  4. Barras, B., et al.: The Coq proof assistant reference manual: version 6.1. Ph.D. thesis, Inria (1997)

    Google Scholar 

  5. Bettini, L.: Implementing Domain-specific Languages with Xtext and Xtend. Packt Publishing Ltd., Birmingham (2016)

    Google Scholar 

  6. Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14

    Chapter  Google Scholar 

  7. Gheorghiu Bobaru, M., Păsăreanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-70545-1_14

    Chapter  Google Scholar 

  8. Broy, M.: Theory and methodology of assumption/commitment based system interface specification and architectural contracts. Formal Methods Syst. Des. 52(1), 33–87 (2018). https://doi.org/10.1007/s10703-017-0304-9

    Article  MATH  Google Scholar 

  9. Broy, M., Stølen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, Heidelberg (2012)

    MATH  Google Scholar 

  10. Brucker, A.D., Wolff, B.: A proposal for a formal OCL semantics in Isabelle/HOL. In: Carreño, V.A., Muñoz, C.A., Tahar, S. (eds.) TPHOLs 2002. LNCS, vol. 2410, pp. 99–114. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45685-6_8

    Chapter  MATH  Google Scholar 

  11. Chilton, C., Jonsson, B., Kwiatkowska, M.: Assume-guarantee reasoning for safe component behaviours. In: Păsăreanu, C.S., Salaün, G. (eds.) FACS 2012. LNCS, vol. 7684, pp. 92–109. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35861-6_6

    Chapter  Google Scholar 

  12. Cimatti, A., Dorigatti, M., Tonetta, S.: OCRA: a tool for checking the refinement of temporal contracts. In: 2013 28th IEEE/ACM International Conference on Automated Software Engineering (ASE), pp. 702–705, November 2013

    Google Scholar 

  13. Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97(P3), 333–348 (2015). https://doi.org/10.1016/j.scico.2014.06.011

    Article  Google Scholar 

  14. Clarke, E.M., Long, D.E., McMillan, K.L.: Compositional model checking. In: 1989 Proceedings of Fourth Annual Symposium on Logic in Computer Science, pp. 353–362. IEEE (1989)

    Google Scholar 

  15. Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45–80 (2001)

    Article  Google Scholar 

  16. Damm, W., Hungar, H., Josko, B., Peikenkamp, T., Stierand, I.: Using contract-based component specifications for virtual integration testing and architecture design. In: 2011 Design, Automation & Test in Europe, pp. 1–6. IEEE (2011)

    Google Scholar 

  17. De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011). https://doi.org/10.1145/1995376.1995394

    Article  Google Scholar 

  18. Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Proceedings of the 1999 International Conference on Software Engineering (IEEE Cat. No. 99CB37002), pp. 411–420. IEEE (1999)

    Google Scholar 

  19. Elkader, K.A., Grumberg, O., Păsăreanu, C.S., Shoham, S.: Automated circular assume-guarantee reasoning. In: Bjørner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 23–39. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19249-9_3

    Chapter  Google Scholar 

  20. Emmi, M., Giannakopoulou, D., Păsăreanu, C.S.: Assume-guarantee verification for interface automata. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 116–131. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_10

    Chapter  Google Scholar 

  21. Fensel, D., Schnogge, A.: Using KIV to specify and verify architectures of knowledge-based systems. In: Automated Software Engineering, pp. 71–80, November 1997

    Google Scholar 

  22. Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-14806-9_2

    Chapter  Google Scholar 

  23. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)

    MATH  Google Scholar 

  24. Huber, F., Schätz, B., Schmidt, A., Spies, K.: AutoFocus—a tool for distributed systems specification. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 467–470. Springer, Heidelberg (1996). https://doi.org/10.1007/3-540-61648-9_58

    Chapter  Google Scholar 

  25. Kugele, S., Marmsoler, D., Mata, N., Werther, K.: Verification of component architectures using mode-based contracts. In: 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design, MEMOCODE 2016, Kanpur, India, 18–20 November 2016, pp. 133–142. IEEE (2016). https://doi.org/10.1109/MEMCOD.2016.7797758

  26. Li, Y., Sun, M.: Modeling and analysis of component connectors in Coq. In: Fiadeiro, J.L., Liu, Z., Xue, J. (eds.) FACS 2013. LNCS, vol. 8348, pp. 273–290. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-07602-7_17

    Chapter  Google Scholar 

  27. Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architectures. Sci. Ann. Comput. Sci. 26(2), 187–248 (2016)

    MathSciNet  MATH  Google Scholar 

  28. Marmsoler, D.: A framework for interactive verification of architectural design patterns in Isabelle/HOL. In: Sun, J., Sun, M. (eds.) ICFEM 2018. LNCS, vol. 11232, pp. 251–269. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02450-5_15

    Chapter  Google Scholar 

  29. Marmsoler, D.: Hierarchical specification and verification of architectural design patterns. In: Russo, A., Schürr, A. (eds.) FASE 2018. LNCS, vol. 10802, pp. 149–168. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89363-1_9

    Chapter  Google Scholar 

  30. Marmsoler, D.: Verifying dynamic architectures using model checking and interactive theorem proving. In: Becker, S., Bogicevic, I., Herzwurm, G., Wagner, S. (eds.) Software Engineering and Software Management 2019, pp. 167–169. Gesellschaft für Informatik e.V., Bonn (2019). https://doi.org/10.18420/se2019-52

  31. Marmsoler, D., Blakqori, G.: APML: An architecture proof modeling language. https://arxiv.org/abs/1907.03723, July 2019. Extended preprint

  32. Marmsoler, D., Gidey, H.K.: FACTum studio: a tool for the axiomatic specification and verification of architectural design patterns. In: Bae, K., Ölveczky, P.C. (eds.) FACS 2018. LNCS, vol. 11222, pp. 279–287. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-02146-7_14

    Chapter  Google Scholar 

  33. Marmsoler, D., Gleirscher, M.: Specifying properties of dynamic architectures using configuration traces. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 235–254. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-46750-4_14

    Chapter  MATH  Google Scholar 

  34. Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45949-9

    Book  MATH  Google Scholar 

  35. Obeo: Sirius. https://www.eclipse.org/sirius/

  36. Păsăreanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: a comparative case study. In: Dams, D., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol. 1680, pp. 168–183. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48234-2_14. http://dl.acm.org/citation.cfm?id=645879.672067

    Chapter  Google Scholar 

  37. Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13, pp. 123–144. Springer, Berlin (1985). https://doi.org/10.1007/978-3-642-82453-1_5

    Chapter  Google Scholar 

  38. Reif, W.: The Kiv-approach to software verification. In: Broy, M., Jähnichen, S. (eds.) KORSO: Methods, Languages, and Tools for the Construction of Correct Software. LNCS, vol. 1009, pp. 339–368. Springer, Heidelberg (1995). https://doi.org/10.1007/BFb0015471

    Chapter  Google Scholar 

  39. Reussner, R.H., Becker, S., Firus, V.: Component composition with parametric contracts. In: Tagungsband der Net. ObjectDays 2004, pp. 155–169 (2004)

    Google Scholar 

  40. Spichkova, M.: Focus on Isabelle: from specification to verification. In: 21st International Conference on Theorem Proving in Higher Order Logics, p. 104. Citeseer (2008)

    Google Scholar 

  41. Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education, London (2008)

    Google Scholar 

  42. Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley Object Technology Series (1998)

    Google Scholar 

  43. Wenzel, M.: The Isabelle/Isar reference manual (2004)

    Google Scholar 

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

    Google Scholar 

Download references

Acknowledgments

We would like to thank Simon Foster and Mario Gleirscher for inspiring discussions about APML. Parts of the work on which we report in this paper was funded by the German Federal Ministry of Education and Research (BMBF) under grant no. 01Is16043A.

Author information

Authors and Affiliations

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

    Diego Marmsoler & Genc Blakqori

Authors
  1. Diego Marmsoler
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Genc Blakqori
    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. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Macquarie University, Sydney, NSW, Australia

    Annabelle McIver

  3. University of Minho, Braga, Portugal

    José N. Oliveira

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Marmsoler, D., Blakqori, G. (2019). APML: An Architecture Proof Modeling Language. In: ter Beek, M., McIver, A., Oliveira, J. (eds) Formal Methods – The Next 30 Years. FM 2019. Lecture Notes in Computer Science(), vol 11800. Springer, Cham. https://doi.org/10.1007/978-3-030-30942-8_36

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30942-8_36

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30941-1

  • Online ISBN: 978-3-030-30942-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation