=Paper=
{{Paper
|id=Vol-1294/paper4
|storemode=property
|title=Specifying and Verifying Aspect-Oriented Systems in Rewriting Logic
|pdfUrl=https://ceur-ws.org/Vol-1294/paper4.pdf
|volume=Vol-1294
|dblpUrl=https://dblp.org/rec/conf/icaase/BoudjedirBM14
}}
==Specifying and Verifying Aspect-Oriented Systems in Rewriting Logic==
https://ceur-ws.org/Vol-1294/paper4.pdf
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
Specifing and Verifing Aspect-Oriented
Systems in Rewriting Logic
1 2
Amina BOUDJEDIR Toufik BENOUHIBA , Djamel MESLATI
LISCO Laboratory, Department of computer science LISCO Laboratory, Department of computer science
Badji Mokthar University. Annaba, Algeria Badji Mokthar University. Annaba, Algeria
1
a.boudjedir@hotmail.fr toufik.benouhiba@gmail.com
2
meslati_djamel@yahoo.com
Abstract – Aspect-oriented (AO) systems have to deal with an important problem which is the management of
aspect interaction. In this paper, we introduce a first tool, known as AO-Maude, which is based on Maude
language for the specification and the verification of the AO systems. The proposed tool relies on the
reflection feature of rewriting logic that allows us to represent in the Meta-Level the structure of the base
system, aspects and the weaver mechanism. The contributions of this paper are twofold. First, we provide a
support for the specification of the AO systems in Maude language and thus discharge the user from the task
of the definition of the weaver mechanism each time. Second, our extension offers a support to the AO
systems in Maude while managing the aspect interaction problem in general and the scheduling problem in
particular. The proposed tool is illustrated with a concrete case study.
Keywords – Aspect-oriented system; aspect interaction; Aspect-UML; rewriting logic; Maude; Meta-Level;
verification
1. INTRODUCTION
some aspects [2]) and thus unexpected results
Aspect-oriented (AO) systems have been can emerge. In the AO, this issue is commonly
proposed to capture transversal preoccupations. known as the aspect interaction problem [1, 3].
They are considered as a necessary In fact, there are many kinds of aspect
complementarity to the object oriented systems interaction problem: dependence, scheduling,
[1]. Generally speaking, an AO application is redundancy, etc [1]. For example, the
composed of two parts: Base system to scheduling problem, which is the subject of this
implement the system functions and Aspects to paper, occurs when many independent aspects
implement the Cross-cutting concerns. An are concerned by the same joint point. In this
Aspect also consists of two parts: pointcut and case, the execution of these aspects may have
advice. A pointcut is a set of many join points some undesirable effect on the base system if
where an advice should be executed. An advice they are executed in any order. Some of these
is the behavior of an aspect. It can be executed orders can interact badly with the properties of
before, after or around the join point that has the base system. In such circumstances, the
been selected by a pointcut. The AO weaver aspects interfere with each other in a potentially
ensures the integration of the base system and undesired manner and they can be used in a
aspects functionality. harmful way that invalidates desired properties
However, AO weaver can drastically change the and thus change the semantic of the base
semantic of the base system (e.g. some system. Note however that the presence of this
properties can be affected by the introduction of
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 36
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
conflict does not lead necessarily to a violation we propose in [17] a rewriting system [18] in
of base system properties. order to verify and detect bad aspect interaction.
We used the Aspect-UML [15] which is a UML
Many works have tried to tackle this problem in profile that extends the classic UML use case
different ways. By using the model-checking and class diagrams with different concepts of
technique, several approaches have been AO. We translated the base system of the
proposed for the verification of aspect-oriented Aspect-UML models into Maude [19]
systems. The authors of [4] define incremental specifications. Then the aspects and their
aspect model-checking which consisted to subsequent concepts are translated into Maude
modularize the verification of aspects (i.e. verify specification. Finally, a weaving step is defined
properties against aspect without having access in order to integrate the aspects into the base
to the program source). The authors of [5] system. Afterwards, all these specifications are
present an approach for modeling and verifying formally verified by the Maude tool in order to
aspect-oriented systems with finite state detect possible conceptual errors concerning
machines. They define class and aspect models aspect interactions. Although, the result of the
with state machines. These models are then proposed approach helps us to detect bad
composed and weaved into a final model via aspect interaction, the implementation of the
weaving mechanism. Once the model that approach contains some messy code. In fact, in
represents the entire system is generated, they the early proposed approach the user specifies
proceed to verify the system against the desired not only the aspect models, but also the aspect
system properties by using the LTSA (Labelled composition and the weaver process. This later
Transition System Analyser) model checker [6]. makes the task very tedious to do it each time.
However, the weaving process was not
rigorously defined and the authors did not In this work, we aim to provide a support that
consider the scheduling problem since they hides all the details of the weaver. The user thus
suppose a predefined execution order. Another cares only about the specification of the base
attempt for the formal verification of the aspect- system and aspect. This support is an extension
oriented systems exploits the techniques of of the rewriting systems in general and of Maude
model checking. We can cite the proposed language in particular for the specification and
approach of [7]. This approach builds the aspect verification of Aspect-UML models. This
model and verifies the deadlock problem with extension is realized as a first AO-Maude
Spin model checker [8]. In a series of papers [9, support. This one relies on the reflection feature
10, 11], Katz and his group have addressed of Maude system which allows us to represent in
various issues of model checking aspect- the Meta-Level: the general form of base system
oriented code. For instance in [11], the authors and aspects of the Aspect-UML models, the
suggest an assume-guarantee structure to processing of the aspect composition and the
achieve modular and generic verification of AO weaver mechanism. The user represents only
systems. They verify that for any base state the Aspect-UML models by base and aspect
machine satisfying the assumptions of a given modules. Afterward, he gives the task of the
aspect, the woven state machine is guaranteed composition and integration of the aspects within
to satisfy the desired properties. the base system to the defined weaver. The
result of this composition and integration is
Depending on the source-code level, several examined later in order to detect and verify
works have been proposed in the area of the aspect interaction problem.
static aspect analysis [12, 13] where aspect
conflict can be detected depending on pointcut This paper is organized as follows. In section 2,
definitions. We can also cite the work of [14] in we give an overview on the rewriting logic and
which the authors present a language named the reflective capabilities of the Maude system.
compAr in order to model aspects with around In section 3, we outline the main phases
advices. However, the complexity of the source- adopted in the realization of our support. We
code can be an important drawback of these illustrate, in section 4, the proposed support in a
approaches. In addition, the aspect interaction case study. Finally, section 5 concludes the
problem has to be detected and fixed in early paper.
development stages in order to minimize
maintenance costs.
2. REWRITING LOGIC AND THE META-
Depending on the design level, different LEVEL OF MAUDE
approaches [15, 16, 17,] tried to integrate
aspects within abstract models to ensure early
Rewriting logic is introduced by José Méseguar
detection of interaction problem. For instance, [19]. This logic is a reflective framework for
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 37
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
expressing a very wide range of concurrent integration of the aspects within the base system
systems and languages. Thus, many languages to the defined weaver. As it is shown in Figure 1,
based on this logic (ASF+SDF [20], CafeOBJ the AO-Maude is divided into two parts: what we
[21], Maude have been proposed. have defined in the Meta-level and what the user
should write. The specification of AO-Maude
In this paper, we use Maude language which is follows the following steps:
a specification and programming language. It
allows us to define data types by giving 3.1. Definition of a useful module
signatures and equations. The behavior is
specified by the use of rewrite rules. Maude also The aim of this step is to define a module that
supports the modeling of object oriented specifies the different concepts of the aspect
systems and integrates an LTL model-checker model (i.e. aspect type/sort, attributes sort,
that can be used to verify the required methods sort and general form of advices). All
properties. This modeling and verification is these elements are an extension of other
supported in different ways. Currently, Maude concepts in Maude. The idea behind this
offers two ways (the Core Maude and Full definition is to provide a generic module that can
Maude) to support that. The two ways are be imported at any time by the user as well as
similar but are based on different levels of the some other Maude module (likes the Nat module
language. In addition, Maude language supports for natural number, etc).
some Meta-functionalities [19] that help us to
build new environments and languages by 3.2. Definition of base/aspect modules’
implementing an extension of Maude. Full syntax
Maude is the real example of the extension of
Maude. It endows the language with an even Since the AO-Maude is a first proposed tool, we
more powerful and extensible module algebra agreed to specify all the declarations and
[22]. Full Maude itself can be used as a basis for statements of base and aspect modules in the
further extensions by adding new functionality. It same manner of Maude modules style (i.e. we
is possible both to change the syntax or the keep all the different concepts of these modules
behavior of existing features and to add new such as: sorts, operators, equations, rules, etc).
features. In this way, many concurrent systems This idea allows as not only to avoid the re-
have inspired extensions to different kinds of implementation of the code (i.e. defining new
systems via Full Maude specifications such as: parser and compiler) and thus taking advantage
real-time system [23], probabilistic system [24], of the infrastructure provided, but also to rid the
etc. Thus, since Full Maude offers a way to user of the step of the learning of new syntax.
define new environments and tools; we agreed However, in order to make the deference
to use its functionalities in order to provide an between the Maude modules and AO-Maude
attractive support for the modeling and the (base and aspect) modules, we have enclosed
verification of aspect-oriented systems by the base module body between the keywords
rewriting systems. These features allow us to bmod and endbm and the aspect module body
define not only the weaver mechanism at the between the keywords amod and endam.
Meta-Level, but also to avoid the re-
implementation of the code and thus take 3.3. Transformation of the base/aspect
advantage of the infrastructure provided. modules into ordinary modules
The aim of our work is to provide a support that
3. OVERVIEW ON THE AO-MAUDE allows the user to specify the aspect models and
detect aspect interaction. The detection of
The aim of our work is to define a support in aspect interaction is based essentially of the
which all details of the aspect composition and analysis of the preservation or the violation of
the weaver mechanism are hidden. This is done the pre/postconditions of method/ advice. This
by defining the syntax of each base model, principle has been used in our previewed work
aspect model, aspect composition and the [17], where the user specifies the behavior of
weaver mechanism at the Meta-Level of the AO- each method/advice by two rewriting rules in
Maude. The idea behind this definition is to rid order to detection at the end aspect interaction.
the user from the task of the definition of aspect The first rewriting rule is used in the case where
composition and weaver mechanism each time. the method/advice preconditions are preserved
The user has only to represent the Aspect-UML whereas the second rule is used when these
models by base and aspect modules. Afterward, preconditions are violated. However, we think
he gives the task of the composition and that it would be better to unload the user from
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 38
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
Definition of predefined module
Specification of Aspect Modules’ Transformation of
Syntax Base/Aspect Modules’
Concept to Ordinary
Modules
AO-Maude Detection of
META-LEVEL Specification of Base Modules’ Aspect
Syntax Interaction
Specification of
the Weaver
Specification of Command Syntax Strategy
AO-Maude
OBJECT-LEVEL
Writing Base and Base and Result
Aspect Modules Aspect
Modules
Writing Command
User to check Aspect
Interaction Command
Figure 1: The overall view of AO-Maude
this task because it becomes heavy and tedious 3.4. Definition of the strategies of the weaver
to do it especially when the number of aspect
(advices) and methods is important. The aim of this step is to discharge the user
Consequently, to ensure the detection of the from the task of the definition of the weaver
preservation or the violation of the mechanism each time. Thus, all the messy code
pre/postconditions of method/advice, we agreed of the weaver of [15, 16, 17] will be hidden in the
to define at the Meta-Level some functions that Meta-Level.
handle the rules of each method/advice. These When the user specifies the base system and
functions transform each rule that represents the aspect modules in the first stage, he proceeds,
behavior of each method/advice into two in the second stage, to the step of the
rewriting rules. The first rewriting rule is used in composition and the integration of these aspects
the case where the method/advice preconditions via the base system. This step is guaranteed via
are preserved. In this case the method/advice the internal strategies of the defined weaver. In
can be executed with success whereas the a general way, the different steps of the defined
second rule corresponds to the case where the weaver are the following:
method/advice preconditions are violated. As a
consequence, the execution of the Detecting the invoked joint point during
method/advice leads to an erroneous state. the execution of the base system. The
aim of this step is to detect among the
different base system methods, the method
that represents the join point which is
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 39
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
indicated by the different introduced between the base system methods and the
aspects. advices. Thus, the command tries to verify that:
Collecting the before and after advices The postconditions of the base system
that share the detected join point. To method (it can be a join point) should implies
ensure the execution of the before and after the preconditions of the first advice adv1 as :
advices (note that only before and after post(base)=> pre(adv1) or ;
advices are considered in this paper), we
have used a set of functions that collect the The postconditions of the last advice advn
before and after advices in two different lists. should imply the preconditions of the base
system method (it can be a join point) as:
Permuting the collected before and after post(advn)=> pre(base) .
advices. We have used a set of equations
that helps us to get two lists of all possible
permutation of the before and after advices. 4. CASE STUDY
The idea behind that is to ensure, on one
hand, the non-deterministic composition of To illustrate our work, we present an example
all order of the conflicting advices and, on used in [16] which is a telephony application.
the other hand, the detection of the Figure 2 shows the Aspect-UML class diagram
preservation or the violation of the of this example. The base system, modelled by
pre/postconditions of each advice in each a set of classes, provides core functionalities to
permutation. simulate devices and connections. To these
basic functionalities, aspects can be added,
Composing and integrating the different such as the interrupting callee and the call
advices. We have used a set of functions to forwarding features. These two aspects are
compose and execute each advices used to handling busy lines. They crosscut the
permutation. Thanks to the built-in functions, base system through the pointcut OpComplete
each advice of each permutation is executed which concerns the join point Complete. Note
in the Meta-Level. We have also used a set that this is a typical situation of aspects conflict
of functions to switch between the base because two operations will be added before the
system and the composed advices in order join point and executed in a given order. Figure
to guarantee at the end the integration of the 1 shows how both the aspects are added to
aspect in the base system. enrich the base class diagram.
3.5. Definition of the command that ensure 4.1. Representation of the base system in
the verification of aspect interaction AO-Maude
problem
In the proposed work, the user writes only the
The verification of the composition and the base and aspect modules in the same manner
integration of these advices in the base system as an ordinary Maude module. We present
(which is known as the weaver mechanism) is below a part of connection class as:
guaranteed via our defined command that
follows this principle: bmod CONNECTION is
pr CONFIGURATION .
Principle: Let adv1,…,advn be the advices to be op Connection : -> Cid . ---1 ClassName
executed on a join point, pre(advi) be the op C-Status: C-State ->Attribute. --2 Attributes
op Origin: Oid -> Attribute .
precondition of advi and post(advi) be the op Destination : Oid -> Attribute .
postcondition of advi . Our proposed command op Complete : Oid -> Msg . 3 Methods
tries to ensure the following points: ...
crl : Complete(C1) ---4
Advice-Advice interaction. Our defined
command tries to ensure the interaction
between advices. The verification of the advices =>
ordering consists of verifying that the ---A
postconditions of the advice advi should implies
the preconditions of the advi+1 as : post(advi)=> if State == Disconnected. ---B
pre(advi+1) for every i. endbm
Base-Advice interaction. We aim that the
defined command ensures also the interaction
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 40
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
context Interrupting
<>
pre : Destination. D-Status = Busy
post : Destination. D-Status = Idle Interrupting
post : Destination.Current.C-Status = Interrupted + interruptedC : ListOfConnection
Device Connection before
opComplete (C :Connection)
+ D-Status: String + C-Status: String
2
+ Num : String + Origin : Device
+ Current: Conenction + Destination: Device
<>
+ Pickup()
+ ActivateLigne() opComplete
+ Transmission (num: String)
+ Hangup() +call Connection.Complete
+ Complete ()
+ Tone ()
+ Drop ()
+ Dial (num: String) + opComplete (C )
+ Ring () opComplete: : Binding
ToJoinPoint: Connection. Complete
Binds: C Target <>
context Complete()
pre : C-Status = Disconnected Forwarding
post : C-Status = Connected context Forwarding
post : Origin.D-Status = Disconnected pre :Destination. D-Status = Busy + forwardL : ListOfForwardedNum
post : Destination.D-Status = Disconnected pre : exists (D ) in forwardL
before
post : .Destination = D
opComplete (C :Connection)
Figure 2: A part of the class diagram of the telephony application
The connection class is represented with a base mark 2). The attribute of this aspect is
module. This module should import the represented in the mark 3. The name, the type
Configuration Maude module in order to of this advice and the invoked join point are
represent the main concepts of object-oriented represented with the term DefAdv in mark 4. The
systems. The name of this class is represented specification of the behavior of the advice
by an operator in mark 1. The attributes of this InterruptAdvice is represented with a rewriting
class are represented with operators of sort rule. The pre and postconditions of this advice
Attribute (mark 2). The methods (we take only are respectively represented with the condition
one method) are also represented by operators of the rule and the left hand side of this rule.
as it is shown in mark 3. The behavior of each
method is represented by conditional rewriting amod INTERRUPTING is
pr CONNECTION .
rule (mark 4). The left hand side of this rule pr Asp&Adv-Configuration . ---1
represents the object C1 of class connection op Interrupting : -> Aid . ---2 AspectName
with the actual C-Status State. The Term Op InterruptedC: List{Oid} -> AspAttribute.---3
Complete() means that a message is sent to the Attribute
object C1 asking for the execution of Complete() op InterruptAdvice: -> AdvName . ---AdviceName
...
method. Whereas, the right hand side of this rule crl:
shows the state of the behavior of the object DefAdv
after executing the Complete() method. The pre ---4
and postconditions of the method are
represented respectively by the marks B and A.
4.2. Representation of aspects in AO-Maude
=>
We illustrate in the following a part of the
interrupting aspect of the figure 2. This aspect is
represented by an aspect module where it
should import the Asp&Adv-Configuration AO-
represent the name of aspect (as it is shown in if State == Busy. ...
endam
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 41
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
4.3. Transformation of the base/aspects Remember that our purpose consists of
modules into ordinary Maude modules ensuring the composition and the integration of
all possible advices order and checking if all pre
Once the user has defined the base and aspect and postconditions of the advices and methods
modules, the AO-Maude transforms each are preserved. By using our defined command
module into an ordinary Maude module (as it is CheckExecution, we can verify the composition
shown in section 3 step(3)). Since each and the integration of aspects in the base
introduced base or aspect module is similar to system as:
the Maude module (i.e. all the different concepts
of these modules are kept), the AO-Maude CheckExecution(
transforms only the behavior of each
method/advice (which is represented by one Pickup()
rewriting rule) into two rewriting rules. Note that
this transformation is done in the Meta level and ASPECTs(
with a transparent way to the user. We just < InterruptAdvice : Interrupting | I-Status : Idle
present how the connection class becomes (in >
< ForwardAdvice : Forwarding | F-Status : Idle >
the same manner the different aspects are ))
transformed):
The AO-Maude starts the verification from the
mod CONNECTION is ...
crl : Complete(C1) initial terms of the CheckExecution command. It
tests whether all possible orders of advices can
be executed with success. AO-Maude finds out
=> two possible solutions (since we have only two
advices). In the first solution, we have obtained
a failure execution of the InterruptAdvice. This
ResultExecution(Complete(C1),Success) situation is due to the following: before executing
if State == Disconnected. the join point Complete(), the AO-Maude starts
crl : Complete(C1) the composition of the advices by executing the
InterruptAdvice as the first advice. This advice
interrupts the current connection and changes
=> the status of destination to Idle. Once the
InterruptAdvice ends, the control flow is passed
to the ForwardAdvice. At that time a warning
ResultExecution(Complete(C1),Error) message is printed by the fact that the
if State =/= Disconnected.
endm
... preconditions of this advice are not verified (pre:
Destination. D-Status = Busy, see figure 2).
Thus, the execution of the InterruptAdvice
Since all the concepts (class, attributes and
before the ForwardAdvice leads to the violation
method name) are presented in the same way
of the preconditions of ForwardAdvice. Note that
as they were defined in the base module, this the violation of the pre and/or postconditions
module presents only the transformation of the
does not mean necessarily that the base system
method Complete into two rewriting rules. The
will be halted but we can say that the whole
first rule will be executed when the preconditions
system would be in an incoherent status, which
of this method are preserved (the preconditions
makes it impossible to predict its future states.
should ensure that State is equal to Thus, the execution of the ForwardAdvice
Disconnected), in this case the method is should hence be considered first as it was found
executed with success. Otherwise, the second
in the second solution.
rule will be execute and indicates an error
execution of method. We have used a term
ResultExecution(Complete(),Success/Error) to 5. CONCLUSION
show the successful /failure execution of the
method Complete. In this paper, we have investigated the aspect
interaction problem in general and aspect
4.4. Detection of aspect interaction with the scheduling in particular. We have presented a
defined command
new tool for the modeling and the verification of
aspect-oriented systems in rewriting logic. In this
In this steps, the user proceeds to verify the
tool, reflection feature played a decisive role.
composition and the integration of the aspects in
This tool, which name is AO-Maude, allowed us
the base system (the written classes).
to define in the Meta-Level the structure of base
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 42
ICAASE'2014 Specifing and erifing Aspect-Oriented ystems in ewriting ogic
and aspect modules, weaver mechanism and Foundations of Aspect Languages
new command that ensures the verification of Workshop, Germany, 2006.
the composition and the integration of aspects in [12] R. Douence, P. Fradet, and M. Sudholt,
the base system. “Composition, reuse and interact analysis of
stateful aspects”, International Conference
By using the new command in a case study, it is AOSD, pp.141–150, 2004.
possible to check whether the interaction of [13] M. Störzer and J. Krinke, “Interference
aspects affects either their properties or the analysis for AspectJ”. Workshops on
base system properties. Foundations of Aspect-Oriented Languages,
2003.
The current tool can be improved in different
ways. The first idea is to extend this tool by [14] R. Pawlak, L. Duchien and L. Seinturier,
“CompAr: Ensuring Safe Around Advice
integrating the around advices and considering Composition”, International Conference on
more general kind of pointcuts by defining them Formal Methods for Open Object-Based
on aspects. We can also define other Distributed Systems, France, 2005.
commands that helps us to display the search [15] F. Mostefaoui , “Un cadre formel pour le
graph generated by the last search. développement orienté aspect :
modélisation et vérification des interactions
dues aux aspects” , PhD thesis, Canada,
6. REFERENCES 2008.
[16] F. Mostefaoui and J. Vashon, “Design-level
[1] R. Pawlak, J.P. Retaillé and L. Seinturier, Detection of Interactions in Aspect UML
“Programmation orientée aspect pour models using Alloy”, Journal of Object
Java/J2EE”, First Edition, Paris, 2004. Technology, vol.6, pp 137-165, 2007.
[2] S. Djoko Djoko, R. Douence and P. Fradet, [17] A. Boudjedir, T. Benouhiba and D. Meslati,
“Aspects Preserving Properties”, ACM “Verification of aspect composition and
Press, Vol. 3, pp.393-422, 2012. integration using rewriting systems”, the
International Symposium on Modelling and
[3] K. Tian, k. Cooper, K. Zhang and H. Yu, “A Implementation of Complex Systems,
Classification of Aspect Composition pp.138-148. Algeria , 2010.
Problems”, IEEE International Conference
SSIRI. Shanghai, pp. 101-109, 2009. [18] N. Dershowitz and J.P. Jouannaud, “Rewrite
Systems”, Formal Models and Semantics,
[4] S. Krishnamurthi, K. Fisler and M. North-Holland, pp.243-320, 1990.
Greenberg, “Verifying aspect advice
modularly”, ACM SIGSOFT Symposium on [19] M.Clavel, F.Durán, S.Eker, P. Lincoln, N.
Foundations of Software Engineering, USA, Marti-Oliet, J. Meseguer and C. Talcott.
pp.137-146, 2004. “Maude Manual (Version 2.6)”, SRI, 2011.
[5] D.X. Xu, O. El-Ariss, W.F. Xu, and L.Z. [20] A.V. Deursen, J. Heering and P. Klint,
Wang, “Aspect-Oriented Modeling and “Language Prototyping: An Algebraic
Verification with Finite State Machines”, Specification Approach”, W. Scientific, 1996.
Journal of computer science and
technology, pp.949-961, 2009. [21] K. Futatsugi and R. Diaconescu, “CafeOBJ
Report”, W.Scientific, 1998.
[6] LTSA Web Site:
http://www.doc.ic.ac.uk/ltsa/. [22] F. Duran, “A Reflective Module Algebra with
Applications to the Maude Language”, PhD
[7] G. Denaro and M. Monga, “An Experience thesis, University of Malaga, Spain, 1999.
on Verification of Aspect Properties”. The
International Workshop on Principles of [23] P.C. Olveczky, “Specification and Analysis
Software Evolution, Austria, 2001. of Real-Time and Hybrid Systems in
Rewriting Logic”, Thesis, 2000.
[8] G.J Holzmann, “The model-checker SPIN”,
IEEE Transcripts on Software Engineering, [24] G. Agha, J. Meseguer and K. Sen,
pp. 01-17, 1997. “PMaude: Rewrite-based specification
language for probabilistic object systems”.
[9] S. Katz and M. Sihman, “Aspect-validation Workshop on Quantitative Aspects of
using model-checking”, the International Programming Languages, 2005.
Symposium on Verification, Springer,
pp.389-411, 2003.
[10] M. Sihman and S. Katz, “Model checking
applications of aspects and
superimpositions”, Foundations of Aspect
Oriented Languages, Bonn, Germany,
pp.51-60, 2003.
[11] M. Goldman, and S. Katz, “Modular generic
verification of LTL properties for aspects”.
International Conference on Advanced Aspects of Software Engineering
ICAASE, November, 2-4, 2014, Constantine, Algeria. 43