Hierarchical Verification in Maude of LfP Software Architectures

  • Chadlia Jerad
  • Kamel Barkaoui
  • Amel Grissa Touzi
Part of the Lecture Notes in Computer Science book series (LNCS, volume 4758)


Software architecture description languages allow software designers to focus on high level aspects of an application by abstracting from details. In general, a system’s architecture is specified in a hierarchical way. In fact, hierarchical components hide, at each level, the complexity of the sub-entities composing the system. As rewriting logic is a natural semantic framework for representing concurrency, parallelism, communication and interaction, it can be used for systems specification and verification. In this paper, we show how we can take advantage of hierarchical modeling of software systems specified with LfP, to prototype model checking process using Maude system. This approach allows us to hide and show, freely and easily, encapsulated details by moving between hierarchical levels. Thus, state explosion problem is mastered and reduced. In addition, system’s maintainability and error detection become easier and faster.


Hierarchical Level Software Architecture Linear Temporal Logic Evaluation Mark Architecture Description Language 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Garlan, D.: Software architecture. Encyclopedia of Software Engineering, School of computer science, Carnegie Mellon University (2001)Google Scholar
  2. 2.
    Leucker, M.: Rewriting logic as a framework for building generic tools for verifying concurrent systems. RWTH Aachen, Germany (1998), URL:
  3. 3.
    Clavel, M., et al.: Maude manuel (version 2.1) (March 2004)Google Scholar
  4. 4.
    Malcolm, G., Goguen, J.: Proving correctness of refinement and implementation. Technical report, Oxford University (January 1996)Google Scholar
  5. 5.
    Gilliers, F.: Développement par prototypage et Généation de Code à partir de LfP, un langage de modélisation de haut niveau. PhD thesis, Pierre et Marie Curie University, Paris VI, France (2005)Google Scholar
  6. 6.
    Jerad, C., Barkaoui, K.: On the use of rewriting logic for verification of distributed software architecture description based lfp. In: Proceedings the 16th IEEE International Workshop on Rapid System Prototyping, Montreal, Canada, June 2005, pp. 202–208. IEEE Computer Society Press, Los Alamitos (2005)CrossRefGoogle Scholar
  7. 7.
    Jerad, C., Barkaoui, K., Grissa Touzi, A.: Vérification des architectures de systmes distribués par utilisation du ltl model checker de maude. In: 8th African Conference on Research in Computer Science, Cotonou, Benin, pp. 99–106 (November 2006)Google Scholar
  8. 8.
    Richard, N., Medvidovic, N., Taylor: A classification and comparison framework for software architecture description languages. IEEE Transactions on Software Engineering 26(1) (January 2000)Google Scholar
  9. 9.
    Kenney, J.J.: Executable Formal Models of Distributed Transaction Systems Based on Event Processing. PhD thesis, Department of Electrical Engineering, Stanford University, USA (June 1996)Google Scholar
  10. 10.
    Allen, R.J.: A Formal Approach to Software Architecture. PhD thesis, School of Computer Science, Carnegie Mellon University, USA (May 1997)Google Scholar
  11. 11.
    Regep, D., Kordon, F.: LfP: A specification language for rapid prototyping of concurrent systems. In: 12th International Workshop on Rapid System Prototyping, Monterey, California, pp. 90–96 (2001)Google Scholar
  12. 12.
    Meseguer, J.: Rewriting as a unified model of concurrency. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 384–400. Springer, Heidelberg (1990)Google Scholar
  13. 13.
    Meseguer, J.: Rewriting logic as a semantic framework for concurrency. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)Google Scholar
  14. 14.
    Marti-Oliet, N., Meseguer, J.: Rewriting logic: Roadmap and bibliography. Theoretical Computer Science (June 2001)Google Scholar
  15. 15.
    Gilliers, F.: Description de la sémantique du langage LfP. Work document, RNTL MOSE Project MORSE-SRS-031114-V0.15-FGI, Pierre et Marie Curie University, LIP6, France (June 2003)Google Scholar
  16. 16.
    MORSE project web site,
  17. 17.
    Wegmann, A., Naumenko, A.: Conceptual modelling of complex systems using an rm-odp based ontology. In: 5th International Enterprise Distributed Object Computing Conference, Seattle, USA, pp. 27–34 (September 2001)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Chadlia Jerad
    • 1
  • Kamel Barkaoui
    • 2
  • Amel Grissa Touzi
    • 1
  1. 1.LSTS - ENIT, BP 37, le Belvedere 1002 Tunis, Tunisia 
  2. 2.CEDRIC - CNAM, 292, Rue Saint-Martin Paris 75003France

Personalised recommendations