APML: An Architecture Proof Modeling Language

  • Diego MarmsolerEmail author
  • Genc Blakqori
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11800)


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.


Compositional verification Interactive Theorem Proving Architecture-based Verification FACTum Isabelle 



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.


  1. 1.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Math. Struct. Comput. Sci. 14(03), 329–366 (2004)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Baier, C., Katoen, J., Larsen, K.: Principles of Model Checking. MIT Press (2008).
  3. 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). Scholar
  4. 4.
    Barras, B., et al.: The Coq proof assistant reference manual: version 6.1. Ph.D. thesis, Inria (1997)Google Scholar
  5. 5.
    Bettini, L.: Implementing Domain-specific Languages with Xtext and Xtend. Packt Publishing Ltd., Birmingham (2016)Google Scholar
  6. 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). Scholar
  7. 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). Scholar
  8. 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). Scholar
  9. 9.
    Broy, M., Stølen, K.: Specification and Development of Interactive Systems: Focus on Streams, Interfaces, and Refinement. Springer, Heidelberg (2012)zbMATHGoogle Scholar
  10. 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). Scholar
  11. 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). Scholar
  12. 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 2013Google Scholar
  13. 13.
    Cimatti, A., Tonetta, S.: Contracts-refinement proof system for component-based embedded systems. Sci. Comput. Program. 97(P3), 333–348 (2015). Scholar
  14. 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. 15.
    Damm, W., Harel, D.: LSCs: breathing life into message sequence charts. Formal Methods Syst. Des. 19(1), 45–80 (2001)CrossRefGoogle Scholar
  16. 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. 17.
    De Moura, L., Bjørner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011). Scholar
  18. 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. 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). Scholar
  20. 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). Scholar
  21. 21.
    Fensel, D., Schnogge, A.: Using KIV to specify and verify architectures of knowledge-based systems. In: Automated Software Engineering, pp. 71–80, November 1997Google Scholar
  22. 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). Scholar
  23. 23.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming, vol. 14. Prentice Hall, Englewood Cliffs (1998)zbMATHGoogle Scholar
  24. 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). Scholar
  25. 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).
  26. 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). Scholar
  27. 27.
    Marmsoler, D., Gleirscher, M.: On activation, connection, and behavior in dynamic architectures. Sci. Ann. Comput. Sci. 26(2), 187–248 (2016)MathSciNetzbMATHGoogle Scholar
  28. 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). Scholar
  29. 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). Scholar
  30. 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).
  31. 31.
    Marmsoler, D., Blakqori, G.: APML: An architecture proof modeling language., July 2019. Extended preprint
  32. 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). Scholar
  33. 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). Scholar
  34. 34.
    Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). Scholar
  35. 35.
  36. 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). Scholar
  37. 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). Scholar
  38. 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). Scholar
  39. 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. 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. 41.
    Steinberg, D., Budinsky, F., Merks, E., Paternostro, M.: EMF: Eclipse Modeling Framework. Pearson Education, London (2008) Google Scholar
  42. 42.
    Warmer, J.B., Kleppe, A.G.: The Object Constraint Language: Precise Modeling with UML. Addison-Wesley Object Technology Series (1998)Google Scholar
  43. 43.
    Wenzel, M.: The Isabelle/Isar reference manual (2004)Google Scholar
  44. 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

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Technische Universität MünchenMunichGermany

Personalised recommendations