ICAASE'2014 K-Maude Definition of Dynamic Software Architecture K-Maude Definition of Dynamic Software Architecture Sahar Smaali, Aïcha Choutri, Faïza Belala LIRE Laboratory, Constantine 2 University, Algeria sahar.smaali@gmail.com, aichachoutri@gmail.com, belalafaiza@hotmail.com Abstract – One of the complex issues in developing architectural models of software systems is the capturing of architectures dynamics, i.e., systems for which composition of interacting components, changes at run time. In this paper, we argue that it is possible and valuable to provide a Dynamic Software Architecture Meta-model (DySAM) that accounts for interactions between architectural components and their reconfiguration. The key to the proposed approach is to use a graphical notation, according to MDA approach, and a Maude semantic basis using the K framework for both dynamic software architecture elements reconfiguration and steady-state behavior. Keywords –DySAM, Dynamic Software Architecture (DSA), Operational semantics, K framework in terms of evolution rules. However, despite its 1. INTRODUCTION completeness to cover all DSA aspects, DySAM model, like any other meta-model, is not self- Dynamic software architectures (DSA) are those sufficient to support its behavioral semantics architectures that modify their structure and (usually called operational semantics). Indeed, behavior and enact the modifications during the this meta-model supports an observational system’s execution without stopping the (structural and static) semantics only (via application. This behavior, commonly known as associations’ multiplicities, constraints) and lacks run-time evolution or dynamism (reconfiguration), a built-in support for defining semantics of both is widely considered one of the most crucial behavior and evolutionary changes. features of modern software systems. It needs a On the other hand, integrations between formal flexible development strategy so that the and visual (graphical) modelling specifications underlying systems preserve their well- are attracting increasing interest due to their functioning over time by managing themselves benefits. Combining these two approaches, may their evolution [1]. show how the advantages of one approach can In a previous work [2], we proposed a solution to be exploited to cover or weaken the address the above challenges in the meta- disadvantages of the other. In fact, combined modelling context according to the MDA models can make formal methods easier to apply approach. It is an alternative definition of and informal ones more precise [3]. Software architecture in terms of a complete In this paper, we aim to define DySAM meta-model called DySAM (Dynamic Software operational semantics by integrating the meta- Architecture Meta-model) that promotes the use model in K framework |4]. This later is a semantic of interfaces as the primary artefact to be framework in which, programming languages, specified and maintained. It offers to architects calculi, as well as type systems or formal familiar modelling concepts and notations to analysis tools can be defined. It is based on define their applications’ structure, behavior and Maude [5], a rewriting logic based language, dynamism. Indeed, it defines the interactions dedicated to specify concurrent state changes. between architectural elements in terms of data transactions as well as their evolution strategies International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 92 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture The main advantages of our approach are: provide a basis for rigorous properties analysis of the software system at an architecture abstract  It provides lightweight and more intuitive level. However, they remain uncommon and they graphical notations, which are more familiar are not well appreciated by designers and and user-friendly. engineers.  It gives formal specification and verification tools, which are easy to use in the Besides, a third class of hybrid approaches [10], development lifecycle of the software to which our work belongs, may also be architecture. considered, they specify DSA as models having two possible forms, a graphical one intended to  It provides DSA models with formal and visualize SA elements and a theoretical form, rigorous semantics thanks to K framework usually used to allow reasoning and formal use. This important advantage defines a meta-transformation closely conform to the analysis of DSA. Thus, hybrid approaches take MDA model transformation principle. benefits of both models and formal methods.  It allows transparent execution of DSA In the same thought, our contribution consists in models in Maude, so that model validation defining DSA according to the MDA meta- and verification can be performed using modeling approach and then, integrating this transparently its tools such as Model- definition in the formal K framework. We define Checker. DySAM operational semantics with K-Maude tool, in order to facilitate execution and The remainder of the paper is organized as verification of the DSA by users not familiar with follow: In section 2, we position our approach Maude language concepts. In fact, K allows a among existing ones. Section 3 presents an transparent passage from the SA description to overview of our meta-model DySAM for DSA its Maude based executable model. description and basic concepts of K framework. In section 4, we explain how we integrate 3. Prerequisites DySAM in K and define its operational semantics. The paper is then concluded in In this section, first, we present our developed section 5 by drawing some comments and meta-model for dynamic software architecture outlining some perspectives for future work. (DySAM) [2], based on interfaces as first class entity, then, we introduce some basic concepts of K system. 2. Related Work 3.1. DySAM Model Some recent research efforts have adapted existing modeling notations and formal In all proposed SA definitions (namely those specification techniques (Process algebra, Petri given by ADL or related to component based nets, etc.) to specify dynamic software models); the interface concept is the key element architecture of a given system, while others have characterizing or even identifying an architectural developed new languages specifically for the element [2]. In fact, components are composed purpose new architecture description languages. only through their interfaces and connector In this section, we divide the existing work into interfaces specify participant roles in an modelling/meta-modelling approaches, and interaction. Interfaces support a part of those merely based on formal methods. architectural elements semantics and behavior The first ones specify DSA, as a model of allowing the description of dynamic aspects as software systems or a set of features of the well as their constraints. models themselves. They provide familiar and comprehensible notations (usually diagrams and In previous work [2], we have suggested a new graphical notations) to model all software definition of architectural description, primarily architecture aspects (UML [6] and Palladio [7]). based on the interface concept (figure1). Thus, But, few interest is dedicated to model behavior the DySAM model considers it as first class entity while leaving components and connectors as and dynamics. grey boxes. This will offer more flexibility and a loose coupling of architectural elements. The second class of existing formal specification techniques have also been applied to formalize DySAM maintains both structure and dynamic SA elements and its behavior in a given logic (we behavior of SA. The model elements are not only cite here for instance, formal ADL) [8, 9]. They International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 93 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture Maude [5] modules that are handy in most language definitions, such as ones for defining computations, configurations, environments, stores, etc. The “K-Maude” interface is what the user typically sees: besides usual Maude module (K-Maude fully extends Maude), one can also include K-modules containing syntax, semantics or configuration definitions using the K notation. A first component of K-Maude tool translates K- modules to Maude modules. These later encode K-specific features as meta-data attributes and Figure 1: DySAM model motivation. serve as an intermediate representation of K- definitions. This intermediate representation can structure constructs, comparable to those of be further translated to various back-ends: architecture description languages (ADL), but executable/analyzable Maude modules, which also: can serve as a basis for formal analysis, or LATEX files for documentation reasons.  The interfaces’ behavior as a state transition system. An interface may be either active or passive allowing shutting down a part of the system in order to perform some architectural changes without altering its consistency.  The interactions between the architectural elements in terms of information exchange, in order to analyze and verify the system behavior in the early phases of the software development cycle.  The architecture dynamic evolution as a set Figure 2: The K-Maude architecture. of strategy rules that allow adding, destroying, or even replacing architectural K language definitions are given as K-modules, entities. An evolution manager is responsible entirely inspired from Maude modules. Each K- of applying this rules and maintaining the module includes two sub-modules: one for the coherence of the system. syntax definition and another for the semantics one. This separation reduces ambiguities and DySAM is an Ecore model based on EMF allows parsing a large variety of programs. (Eclipse Modeling framework) [11], a sophisticated meta-modeling framework. Textual Syntax in K is defined using a variant of the and graphical visualization or editors can be built familiar BNF (Backus Naur Form) notation [15], on top of the meta-model thanks to GMF [12] with terminals enclosed in quotes and non- and Xtext [13] tools. terminals starting with capital letters. The syntax is similar to that of standard Maude syntax (sorts, 3.2. K framework sub-sorts and mix fix operation declarations). However, in addition to Maude’s attributes (such K was initiated by Grigore Rosu in 2003 and as precedence and gathering), specific K- completely developed in 2010 [4]. It is a semantic attributes can be added, such as strict, which is framework based on rewriting logic. It provides used to specify that some arguments of a executable Maude specifications for language construct must be evaluated first (and programming languages and formal analysis their effects on the global state are propagated) tools using configurations, computations and before giving a semantic to the construct itself. rules. Its general objective is to demonstrate that a formal specification language for these A language semantics specification in K consists systems can be simple, expressive, analyzable, of three parts: and executable at the same time [14].  Providing evaluation strategies, otherwise K strategies specify the evaluation order of the Figure 2 presents the K framework architecture. arguments. The gray arrows denote translator tools  Giving the structure of the configuration that implemented as part of the K framework toolkit. holds the program state. Configurations are The file “k-prelude.maude” contains several structured as nested labeled cells (using an International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 94 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture XML-like notation) containing various Thus, we follow the same steps as for the computation-based data structures. programming languages. Otherwise, we have to  Writing K-rules to describe transitions define its syntax under BNF notation. Then, we between configurations. define the syntactic K-rules for interpreting DySAM proposed syntax. On the other hand, we The K-Maude tool is designed to well define specify its operational semantics thanks to the operational semantics of programming common configurations and rules sets. K-rules languages. In our paper, we exploit it to define define particularly, the architecture evolution the operational semantics of DySAM model. strategies and interaction. Therefore, we use in a transparent manner the rewriting logic, recognized as a unified semantic 4.1. Syntax Module framework, as a dynamic software architecture basis. In the K method application, we have to provide DySAM syntactic definition under BNF notation. This is integrated in K tool as a syntax module 4. DySAM MODEL INTEGRATION IN K that represents a formal meta-model defining all FRAMEWORK concepts of DySAM. Table 1 describes a part of the DySAM syntax with an illustrative example. A To make formal methods more user-friendly system architecture description starts with the (expand their use), we may combine them with keyword SystemArchitecture and an identifier informal design techniques. In this work, we Id followed by a set of interfaces, attachments, integrate the DySAM model in K, while providing an evolution manager and interactions between an intuitive modeling notation, supporting a braces. Each interface may be a graphical view, but still having a rigorous syntax ComponentInterface, or ConnectorInterface. and semantics. Table 1: A part of DySAM syntax in K Architecture Description Syntax K-Definition SystemArchitecture ::= “SystemArchitecture" Id "{" Interfaces "Attachments{" SystemArchitecture Arch{ Attachments "}" EvolutionManager "Interactions{" Interactions"}" Interfaces ::= Interface >Interfaces Interfaces[left] Interface ::= PrimitiveComponentInterface | PrimitiveConnectorInterface |… PrimitiveComponentInterface A { PrimitiveComponentInterface::= "PrimitiveComponentInterface" Id "{"Component State Ports "}" Component is C1 ; Component ::= "Component is " Id ";" State is Active ; State ::= "State is" StateValue";" StateValue ::= "Active" | "Passive" Port In AIn uses as1 ; Port ::= "Port" Mode PortId "uses" Id ";" Port In AOut uses as2 ; } Ports::= Port > Ports Ports [left] Mode ::= "In"| "Out"| "InOut" PrimitiveConnectorInterface C { PrimitiveConnectorInterface::= "PrimitiveConnectorInterface" Id"{" Connector Connector is RPC1 ConnectorType State Roles "}" ConnectorType is RPC Connector::="Connector is " Id ";" State is Active ; ConnectorType ::="ConnectorType is" Id ";" Role In CIn ; Role ::= "Role" Mode RoleId";" Role Out COut ; } Roles ::= Role > Roles Roles [left] Attachments { Attachment A.AIn to C.COut Attachment ::= "Attachment" Id.PortId "to" Id.RoleId Attachment B.Out to C.CIn } Attachments ::= Attachment > Attachments Attachments [left] EvolutionManager manager{ EvolutionManager ::= "EvolutionManager" Id "{" EvolutionStrategies "}" EvolutionStrategy S1( X:A ,Y:C){ EvolutionStrategies ::= EvolutionStrategy >EvolutionStrategiesEvolutionStrategies [left] EvolutionStrategy ::= "EvolutionStrategy" Id "(" List ")" "{" Rules "}" EvolutionRule R1{ Rules ::= Rule > Rules Rules [left] Actions{ AddComponentInterface X2;} Rule ::="EvolutionRule" Id "{"Actions Conditions Events Transitions"}" Actions ::= Action > Actions Actions [left] Transitions{ Action ::= ActionName Id ";" ... Set State Y to Passive; } ActionName := "AddComponentInterface" | "DeleteComponentInterface"... } Interactions{ Interactions ::= Interaction > Interactions Interactions [left] Interaction "Msg" between B.BOut and Interaction::="Interaction" Data "between" PortId "and" PortsId "through" RolesId "and" A.AIn through C.CIn and C.COut ; RolesId ";" | ... International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 95 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture The basic definition of each interface is related 4.2. Configuration Definition to the associated primitive element (component or connector). The declaration of the first one A configuration in K is a structure of the (respectively second) contains a set of Ports computations context. It is represented as nested (respectively roles). The keyword uses cells containing standard items as environments, specifies provided or required services through a stores or other specific items (corresponding to port. An Attachment relates ports and roles to the given semantics). The program state is typically represented as a configuration term [16]. build a given structure of SA. The interface abstract behavior is defined by a The rewrite mechanism of K updates the given state transition system (State and StateValue configuration repeatedly by using all possible K- keywords). The State attribute of an interface rules. The configuration abstraction process allows one to specify only the minimal context define its state at a given time. We consider two needed for applying a K-rule [16]. kinds of state: Active (e.g. sending or receiving a message or an event) and Passive (e.g. Figure 4 presents a part of the initial nothing happen). The Transition construct configuration of DySAM. It contains three main specifies the possible state changes by cells. The cell contains the whole description providing the new final state using the keywords used by K tool to start the rewriting process. For Set State. instance, the cell describes the software architecture elements, The evolutionmanager contains a set of evolution strategies and interactions. The evolution Strategies (rules’ sets) to determine interfaces cell contains a set of (represented by a when and how architectural elements will star) and change. A Rule is defined by a set of change to represent the Actions, resulting Events, Conditions and structure of each interface, while the state’s Transitions. cell specifies attachments in a configuration. The value of the attributes is set to Interactions models data exchanges between no name (i.e. undefined). interfaces that may be a message, an event, a session, or even a database access. It specifies The cells and store respectively the Source Port that initiates the interaction ports and roles in a map. The cell (output port); target Ports that designates one stores the evolution strategies and rules to be or more receiving ports (input port) and applied. Finally, the sources/targets ports and Source/Target Roles. Interactions allow also an roles, in addition to the data type used in an interface state change according to the interaction, are stored in cells. architecture behavior. The cell stores the application We can elaborate a DySAM model of any configuration at a given time. It may be system by instantiating all its architectural considered as an instance of the architecture. It element. Figure 3 describes an application that contains cells to describe instances of interfaces contains: instances of A, B and C interfaces and attachments, in addition to evolution denoted by the key word New, 2 attachments notifications. instances and a notification to the evolution 4.3. Semantics Module manager for adding a new interface instance A2 of type A and attaching it to the connector The semantics of the DySAM model is defined in interface instance C1. a separate module with rewriting rules. K-rules SystemSys1{ may be computational rules or structural rules. New A1 : A ; Structural rules capture the structural New B1 :B ; rearrangement of SA, so they allow to reorganize New C1 : C ; the configuration. Attachment instance A1. AIn to C1.COut ; Attachment instance B1.BOut to C1.CIn ; Computational rules define semantics of the Notification S1( A2 : A , C1 : C ) from B1 to M; } computational steps while executing the defined system, as the actual state transitions. These Figure 3: A simple example of a system rules are represented (in a latex file for documentation purposes) by colored cells and a International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 96 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture Figure 4: The initial DySAM Configuration black horizontal line separating the right from the and creates a new left side of the rewriting rule. and sets its internal structure described by name, component, state and the empty < port> cell. Once all the declarations are rearranged in the configuration, computational rules may be applied. In the next section, we explain some of these rules. For instance, Figure 6 describes how a new component interface instance I is added to the system’s configuration. I is added by running the action AddComponentInterface|->N. This action is given by the evolution rule R of the Figure 5: A structural K-rule evolution strategy ES. It creates a new instance The structural rule in figure 5 describes the of interface A and sets its name to I, its state to semantics attributed to the declaration of a passive and fills its ports map (if the name of this component-Interface. If component-interface I instance cannot be found in the names map). declaration is the next thing to be evaluated in the cell then the rule replaces I declaration Figure 7 shows the K-rule that performs a state by the Variable PORTS (to be evaluated next), transition of an interface. This transition is International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 97 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture triggered by the evolution rule R. It will change It transmits a message Msg from an output port the state of the interface (A) instance I, from the P of the component interface I to the input role of value SVN to SV. The interface state changing the connector interface J. This rule is applied, should block all incoming transactions to only if an attachment instance is maintained maintain the architecture in a coherent state, between the port and the role, and the interaction without intercepting the system too long. is already defined in the configuration. The interaction cell specifies ports and roles evolved In the same way, the last rule (Figure 8) details a in this interaction and the transmitted data component and connector interfaces interaction. (message) type. Figure 6: A K-rule describing a new interface instance creation Figure 7: A K-rule modeling state transition of an interface instance. Figure 8: A K-rule describing an interaction. International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 98 ICAASE'2014 K-Maude Definition of Dynamic Software Architecture 5. CONCLUSION Logical Framework, vol 4350 of lecture Notes in Computer Science. Springer, 2007. K is a rewrite-based executable semantic [6] OMG Unified Modeling LanguageTM (OMG framework designed for programming languages UML), Superstructure, 2011. definition. In our paper, we have shown how it http://www.omg.org/spec/UML/2.4.1 could also be used in the field of dynamic [7] About Palladio, http://www.palladio- software architectures to fit with semantics, their simulator.com/about_palladio/, 2014. description definition given in a previous work in [8] R. Allen and D. Garlan, “A Formal Basis terms of a general meta-model (DySAM). In fact, for Architectural Connection.” ACM we have combined MDA development Transactions on Software Engineering techniques with the formal K-method in order to and Methodology, vol. 6, no. 3, pages. provide the DySAM model with both an intuitive 213-249, 1997. modeling notation, supporting a graphical view, [9] J. Magee, N. Dulay, S. Eisenbach, and and rigorous syntax and semantics. Any DySAM J. Kramer. “Specifying Distributed syntactical artifact (interface, attachments, ports, Software Architectures.” In Proceedings oles …), has a K-based semantic interpretation. of the Fifth European Software This valuable conjunction has the advantage to Engineering Conference (ESEC’95), make possible the execution and analysis of an Barcelona, September 1995. architecture description in Maude system in a [10] D. Regep, “LfP : Un Langage de transparent manner. Moreover, any architecture Spécification pour Supporter une dynamic evolution or interaction may also be well Démarche de Développement par handled. Our approach could be easily exploited Prototypage pour les Systèmes even by users not familiar with rewriting logic Répartis”, PhD thesis. , Paris VI concepts. They have just to give a model University, 2003 . conform to DySAM. Thus, in this context, K can be considered as a meta-transformation of [11] Eclipse Modeling Framework, (emf). friendly graphical and textual notations to http://www.eclipse.org/modeling/emf/, 2014 unfriendly formal notations easy to exploit. [12] Graphical Modeling Framework (gmf), http://eclipse.org/gmf-tooling/, 2014. Because the transparency is offered by K [13] Xtext, http://www.eclipse.org/Xtext/, 2014. framework even for analysis and verification, as [14] Serbanuta T., Rusoaie A., Lazar D., ongoing work, we aim to integrate and simplify Ellison C., LucanuD., Rosu G., “The K the use of model-checker in system validation Primer (version 2.5)”, Technical Report, and verification in order to guarantee that the January 2012. system model, built according to DySAM, satisfies global properties during its evolution. [15] Garshol L. M., “BNF and EBNF: What are they and how do they work?” 6. REFERENCES http://www.garshol.priv.no/download/text/bnf .html#id2, 2008. [1] T. Mens, S. Demeyer, Software Evolution, [16] A. Arusoaie and T. F. Serbanuta, “a ISBN 978-3-540-76440-3, Springer, 2008. Contextual transformations in K Framework”, K 2011: 2nd International [2] S. Smaali, A. Choutri et F. Belala, “Towards Workshop on the K Framework and its a Meta-Model for Dynamic Applications,” in Applications, 2011. CBSE’14, Lille, France , 2014, in press. [3] S.-K. Kim, D. Burger and D. Carringt, “An MDA Approach Towards Integrating Formal and Informal Modeling Languages,” J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki (Eds.): FM 2005, LNCS 3582, pp. 448–464, 2005. [4] K semantic framework website, http://www.kframework.org/index.php/Main_ Page, 2014. [5] Clavel M., Duràn F., Eker S., Lincoln P., Marti-Oliet N., Meseguer J., and Talcott C. L. “All about Maude”, A High-Performance International Conference on Advanced Aspects of Software Engineering ICAASE, November, 2-4, 2014, Constantine, Algeria. 99