MIstRAL Tool for Middleware Reconfiguration Based on Formal Methods

Organisation:	Universidade Federal de Pernambuco (BRAZIL)
Functionality:	Distributed Systems.
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Period:	2015
Description:	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.
Conclusions:	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.
Publications:	[Rosa-15] Nelson Rosa. "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 CADP Web site in PDF or PostScript [Rosa-17] Nelson Rosa. "Middleware Adaptation through Process Mining". Proceedings of the 31st IEEE International Conference on Advanced Information Networking and Applications AINA'2017 (Taipei, Taiwan), pages 244-251, IEEE, March 2017. Available on-line at: http://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=7920915 or from the CADP Web site in PDF or PostScript
Contact:	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 BRAZIL Tel: (81) 21268430 E-mail: [email protected]
Further remarks:	This tool, amongst others, is described on the CADP Web site: http://cadp.inria.fr/software

Back to the CADP research tools page