Universidade Federal de Pernambuco (BRAZIL)
CADP (Construction and Analysis of Distributed Processes)
Adaptive middleware is a particular kind of middleware whose behaviour
can be modified at runtime without its complete stop. The motivation
for middleware adaptation is based on the need of adapting to changes
of application's requirements or application's behaviour, adapting to
changes of environmental conditions, fixing middleware's bugs or
extending the middleware functionality. MIstRAL (MIddleware
Reconfiguration Aid by formaLism) is a novel approach for building
adaptive middleware systems based on the lightweight use of formal
methods. MIstRAL works at runtime; assumes that the reason for
reconfiguration is the existence of bad behaviour in the middleware
(e.g., deadlock) or changes in the application requirements; uses
formalisms as enabling technology and does not incorporate the
reconfiguration activities into the middleware.
MIstRAL works by reconfiguring the middleware by checking its execution trace against desired properties expressed in a temporal logic. The execution trace includes application's interactions with the middleware (not the application internal behaviour) and all actions performed by the middleware. MIstRAL is implemented in Java and uses the CADP toolbox to check the execution trace. The properties considered are a subset of the temporal property patterns defined by Dwyer et al., formulated in regular alternation-free mu-calculus. The trace is obtained by instrumenting the middleware with a logger that takes responsibility of logging actions executed by the middleware. The trace is formatted by a processor according to the file format accepted by CADP. The formatted log is passed to the checker that invokes CADP to verify the behaviour properties. If a reconfiguration is necessary (i.e., the trace does not satisfy a property), the checker asks for the configurator to perform the reconfiguration plan according to the property that was not satisfied.
The proposed approach was evaluated on an adaptive object-oriented middleware based on the remoting patterns and a simple client/server application on top of it. The experiments show that the overhead caused by the reconfiguration mechanism is very low (1,45%) compared to the service time.
The new contributions of this approach include: the moving of the
adaptation process to an element outside the middleware; the adoption
of a non-invasive approach in which existing middleware systems may be
adapted without be modified; the use of a lightweight formal approach
(based on checking execution traces using CADP) to guide the middleware
adaptation; and the definition of formal properties that specify
anomalies in the functioning of object oriented middleware systems,
which serve as basis for the adaptation process. Despite the large
number of works on middleware formalisation, none of the existing
approaches focuses on practical (lightweight) aspects of the use of
formal methods to guide the adaptation process.
"Middleware Reconfiguration Relying on Formal Methods".
Proceedings of the 15th IEEE International Conference on Computer
and Information Technology; 14th IEEE International Conference on
Ubiquitous Computing and Communications; 13th IEEE International
Conference on Dependable, Autonomic and Secure Computing; 13th IEEE
International Conference on Pervasive Intelligence and Computing
CIT/IUCC/DASC/PICom'2015, IEEE, pages 648--655, October 2015.
Available on-line at: https://doi.org/10.1109/CIT/IUCC/DASC/PICOM.2015.93
or from the VASY FTP site in PDF or PostScript
Nelson Souto Rosa
Universidade Federal de Pernambuco
Centro de Informática
Departamento de Engenharia da Computação
Av. Jornalista Aníbal Fernandes, s/n
Cidade Universitária (Campus Recife)
50.740-560 - Recife - PE
Tel: (81) 21268430
|Further remarks:||This tool, amongst others, is described on the CADP Web Page: http://cadp.inria.fr|