Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Garlan, D.: Software architecture. Encyclopedia of Software Engineering, School of computer science, Carnegie Mellon University (2001)
Leucker, M.: Rewriting logic as a framework for building generic tools for verifying concurrent systems. RWTH Aachen, Germany (1998), URL: citeseer.ist.psu.edu/leucker98rewriting.html
Clavel, M., et al.: Maude manuel (version 2.1) (March 2004)
Malcolm, G., Goguen, J.: Proving correctness of refinement and implementation. Technical report, Oxford University (January 1996)
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)
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)
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)
Richard, N., Medvidovic, N., Taylor: A classification and comparison framework for software architecture description languages. IEEE Transactions on Software Engineering 26(1) (January 2000)
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)
Allen, R.J.: A Formal Approach to Software Architecture. PhD thesis, School of Computer Science, Carnegie Mellon University, USA (May 1997)
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)
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)
Meseguer, J.: Rewriting logic as a semantic framework for concurrency. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, Springer, Heidelberg (1996)
Marti-Oliet, N., Meseguer, J.: Rewriting logic: Roadmap and bibliography. Theoretical Computer Science (June 2001)
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)
MORSE project web site, http://www.lip6.fr/morse/
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)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jerad, C., Barkaoui, K., Grissa Touzi, A. (2007). Hierarchical Verification in Maude of LfP Software Architectures. In: Oquendo, F. (eds) Software Architecture. ECSA 2007. Lecture Notes in Computer Science, vol 4758. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75132-8_13
Download citation
DOI: https://doi.org/10.1007/978-3-540-75132-8_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75131-1
Online ISBN: 978-3-540-75132-8
eBook Packages: Computer ScienceComputer Science (R0)