Universidade Federal de Pernambuco (BRAZIL)
CADP (Construction and Analysis of Distributed Processes)
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.
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.
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.
Nelson Souto Rosa
Centro de Informatica
Universidade Federal de Pernambuco
50732-970 Recife, Pernambuco
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|