×

Hierarchical design rewriting with Maude. (English) Zbl 1347.68072

Roşu, Grigore (ed.), Proceedings of the 7th international workshop on rewriting logic and its applications (WRLA 2008), Budapest, Hungary, March 29–30, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 238, No. 3, 45-62 (2009).
Summary: Architectural Design Rewriting (ADR) is a rule-based approach for the design of dynamic software architectures. The key features that make ADR a suitable and expressive framework are the algebraic presentation and the use of conditional rewrite rules. These features enable, e.g. hierarchical (top-down, bottom-up or composition-based) design and inductively-defined reconfigurations. The contribution of this paper is twofold: we define Hierarchical Design Rewriting (HDR) and present our prototypical tool support. HDR is a flavour of ADR that exploits the concept of hierarchical graph to deal with system specifications combining both symbolic and interpreted parts. Our prototypical implementation is based on Maude and its presentation serves several purposes. First, we show that HDR is not only a well-founded formal approach but also a tool-supported framework for the design and analysis of software architectures. Second, our illustration tailored to a particular algebra of designs and a particular scenario traces a general methodology for the reuse and exploitation of ADR concepts in other scenarios.
For the entire collection see [Zbl 1279.68017].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q42 Grammars and rewriting systems

Software:

CBabel; yEd; SLMC; GraphML; Maude
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Aguirre, N.; Maibaum, T. S.E., Hierarchical temporal specifications of dynamically reconfigurable component based systems, ENTCS, 108, 69-81 (2004)
[2] Baresi, L.; Heckel, R.; Thöne, S.; Varró, D., Style-based modeling and refinement of service-oriented architectures, Software and Systems Modeling, 5, 2, 187-207 (June 2006)
[3] Batory, D. S., Program refactoring, program synthesis, and model-driven development, (Krishnamurthi, S.; Odersky, M., Proceedings of the 16th International Conference on Compiler Constuction (CC’07). Proceedings of the 16th International Conference on Compiler Constuction (CC’07), LNCS, volume 4420 (2007), Springer), 156-171
[4] Brandes, U.; Eiglsperger, M.; Herman, I.; Himsolt, M.; Marshall, M., GraphML progress report: Structural layer proposal, (Proceedings 9th International Symposium on Graph Drawing (GD ’01). Proceedings 9th International Symposium on Graph Drawing (GD ’01), LNCS, volume 2265 (2002), Springer), 501-512 · Zbl 1054.68543
[5] Bruni, R.; Lluch Lafuente, A.; Montanari, U.; Tuosto, E., Service oriented architectural design, (Proceedings of the 3rd International Symposium on Trustworthy Global Computing (TGC’07). Proceedings of the 3rd International Symposium on Trustworthy Global Computing (TGC’07), LNCS, volume 4912 (2007), Springer), 186-203
[6] R. Bruni, A. Lluch Lafuente, U. Montanari, and E. Tuosto. Style based reconfigurations of software architectures. Technical Report TR-07-17, Dipartimento di Informatica, Università di Pisa, 2007. See http://www.albertolluch.com/adr.html; R. Bruni, A. Lluch Lafuente, U. Montanari, and E. Tuosto. Style based reconfigurations of software architectures. Technical Report TR-07-17, Dipartimento di Informatica, Università di Pisa, 2007. See http://www.albertolluch.com/adr.html · Zbl 1169.68306
[7] Bruni, R.; Meseguer, J., Semantic foundations for generalized rewrite theories, Theor. Comput. Sci., 360, 1-3, 386-414 (2006) · Zbl 1097.68051
[8] Caires, L.; Cardelli, L., A spatial logic for concurrency (part I), Information and Computation, 186, 2, 194-235 (2003) · Zbl 1068.03022
[9] Clavel, M.; Durán, F.; Eker, S.; Lincoln, P.; Martí-Oliet, N.; Meseguer, J.; Talcott, C. L., All About Maude — A High-Performance Logical Framework. How to Specify, Program and Verify Systems in Rewriting Logic, LNCS, volume 4350 (2007), Springer · Zbl 1115.68046
[10] Clements, P.; Garlan, D.; Bass, L.; Stafford, J.; Nord, R.; Ivers, J.; Little, R., Documenting Software Architectures: Views and Beyond (2002), Pearson Education
[11] Courcelle, B., The expression of graph properties and graph transformations in monadic second-order logic, (Rozenberg, G., Handbook of Graph Grammars and Computing by Graph Transformation (1997), World Scientific), 313-400
[12] yEd graph editor homepage
[13] Ferrari, G. L.; Hirsch, D.; Lanese, I.; Montanari, U.; Tuosto, E., Synchronised hyperedge replacement as a model for service oriented computing, (de Boer, F. S.; Bonsangue, M. M.; Graf, S.; de Roever, W. P., 4th International Symposium on Formal Methods for Components and Objects (FMCO’05). 4th International Symposium on Formal Methods for Components and Objects (FMCO’05), LNCS, volume 4111 (2005), Springer), 22-43 · Zbl 1196.68025
[14] Fiadeiro, J. L.; Lopes, A.; Bocchi, L., A formal approach to service component architecture, (Proceedins of the 3rd International Workshop on Web Services and Formal Methods (WS-FM’06). Proceedins of the 3rd International Workshop on Web Services and Formal Methods (WS-FM’06), LNCS, volume 4184 (2006), Springer), 193-213
[15] Gansner, E. R.; North, S. C., An open graph visualization system and its applications to software engineering, Software Practice and Experience, 30, 11, 1203-1233 (2000) · Zbl 1147.68782
[16] Habel, A., Hyperedge Replacement: Grammars and Languages (1992), Springer Verlag · Zbl 0787.68066
[17] Hirsch, D.; Montanari, U., Shaped hierarchical architectural design, ENTCS, 109, 97-109 (2004) · Zbl 1271.68120
[18] O. H. Jensen and R. Milner. Bigraphs and mobile processes. Technical Report 570, Computer Laboratory, University of Cambridge, 2003; O. H. Jensen and R. Milner. Bigraphs and mobile processes. Technical Report 570, Computer Laboratory, University of Cambridge, 2003 · Zbl 1321.68126
[19] Jerad, C.; Barkaoui, K.; Grissa-Touzi, A., Hierarchical verification in Maude of LfP software architectures, (Oquendo, F., ECSA. ECSA, Lecture Notes in Computer Science, volume 4758 (2007), Springer), 156-170
[20] (König, B.; Montanari, U.; Gardner, P., Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6-11 June 2004. Graph Transformations and Process Algebras for Modeling Distributed and Mobile Systems, 6-11 June 2004, Dagstuhl Seminar Proceedings, volume 04241 (2005), IBFI: IBFI Schloss Dagstuhl, Germany)
[21] Martí-Oliet, N.; Meseguer, J.; Verdejo, A., Towards a strategy language for Maude, ENTCS, 117, 417-441 (2005)
[22] Meseguer, J.; Palomino, M.; Martí-Oliet, N., Equational abstractions, (Baader, F., Proceedings of the 9th International Conference on Automated Deduction (CADE’03). Proceedings of the 9th International Conference on Automated Deduction (CADE’03), LNCS, volume 2741 (2003), Springer), 2-16 · Zbl 1278.68185
[23] Meseguer, J.; Rosu, G., The rewriting logic semantics project, TCS, 373, 3, 213-237 (2007) · Zbl 1111.68068
[24] Métayer, D. L., Describing software architecture styles using graph grammars, IEEE Transactions on Software Engineering, 24, 7, 521-533 (1998)
[25] Plotkin, G. D., The origins of structural operational semantics, J. Log. Algebr. Program., 60-61, 3-15 (2004) · Zbl 1072.68063
[26] Rademaker, A.; de O. Braga, C.; Sztajnberg, A., A rewriting semantics for a software architecture description language, Electr. Notes Theor. Comput. Sci., 130, 345-377 (2005) · Zbl 1272.68109
[27] Shaw, M.; Garlan, D., Software Architectures: Perspectives on an emerging discipline (1996), Prentice Hall · Zbl 0948.68506
[28] Verdejo, A.; Martí-Oliet, N., Executable structural operational semantics in Maude, Journal of Logic and Algebraic Programming, 67, 1-2, 226-293 (2006) · Zbl 1088.68095
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.