=Paper=
{{Paper
|id=Vol-1294/paper10
|storemode=property
|title=K-Maude Definition of Dynamic Software Architecture
|pdfUrl=https://ceur-ws.org/Vol-1294/paper10.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/SmaaliCB14
}}
==K-Maude Definition of Dynamic Software Architecture==
https://ceur-ws.org/Vol-1294/paper10.pdf
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