Specification and Verification of Middlewares

Organisation:	Universidade Federal de Pernambuco (BRAZIL)
Method:	LOTOS
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	Middleware.
Period:	2007
Size:	n/a
Description:	Middleware specifications are complex systems that must hide the underlying network mechanisms (communication, failures, changes in mobility and traffic, etc.) from the application. The increasing number of services provided by middlewares (e.g., the CORBA specification contains nineteen services) also contributes to the complexity of middleware specifications. This complexity places many challenges to middleware designers, namely how to integrate services in a single product, how to satisfy new requirements of emerging applications, and how to understand the middleware behaviour prior to implementing it. This work proposes a framework for describing the middleware behaviour formally using LOTOS. The framework is message-centric in the sense that basic elements are grouped according to how they act on the message. Four kinds of abstractions of middleware elements are proposed: mappers (e.g., stub and skeletons), multiplexers (e.g., dispatcher), communication (e.g., channels), and storage (e.g., queue and topic). Each element intercepts a message, processes it and forwards it to the next element. These basic abstractions can be composed to build complex middleware systems. The approach is illustrated by the specification of a message-oriented middleware with a client-server architecture similar to CORBA. On the client side, the middleware is composed of stub and channel elements. On the server side, the middleware is more complex, containing a communication element, several skeletons, and a dispatcher that forwards the request to the proper skeleton. CADP is then used for analyzing the correctness of the LOTOS middleware description. For the example of middleware considered, CADP was successfully used to verify the absence of deadlocks.
Conclusions:	The LOTOS formalisation centered on message request instead of middleware layer simplifies the structure of specifications by highly reusing the basic abstractions. The composition of these abstractions is also facilitated by taking into account the order in which they intercept messages. The use of LOTOS enables the designer to verify behavioural properties of middlewares automatically using CADP. Future work includes the specification of more sophisticated communication elements and the handling of middleware services in the composition constraints.
Publications:	[Rosa-Cunha-07-b] Nelson Souto Rosa and Paulo Roberto Freire Cunha. "A Formal Framework for Middleware Behavioural Specification". In ACM SIGSOFT Software Engineering Notes, volume 32, number 2, pages 1-7, 2007. Full version available from the CADP Web site in PDF or PostScript [Rosa-08] Nelson Souto Rosa. "Behavioral Specification of Middleware Systems". In Michael Alexander and William Gardner, editors, Process Algebra for Parallel and Distributed Processing, chapter 6, pages 161-198, Chapman and Hall, 2008.
Contact:	Nelson Souto Rosa Centro de Informatica Universidade Federal de Pernambuco 50732-970 Recife, Pernambuco BRAZIL Email: nsr@cin.ufpe.br
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page