Refining Middleware Functions for Verification Purpose
Jérôme Hugues, Laurent Pautet, École Nationale Supérieure, Des Télécommunications, Fabrice Kordon · 2003
Abstract — The development of real-time, dependable or scal-able distributed applications requires specific middleware that enables the formal verification of domain-specific properties. So far, typical middleware implementations do not directly address these issues. They focus on patterns and frameworks to meet application-specific requirements. Patterns propose a high-level methodology adapted to the description of software components. However, their semantics does not clearly address verification of static or run-time properties. Such issues can be addressed by other formalisms, at the cost of a more refined description. In this paper, we present our current effort to combine both patterns and Petri Nets to refine and then to verify middleware. Our contribution details steps to build Petri Net models from the Broker architectural pattern. This provides a model of middleware and is a first step towards formal middleware verification. I. ISSUES IN MIDDLEWARE DEVELOPMENT Distribution middleware provides description methods, ser-vices and guidelines to ease the development of distributed applications. Middleware specifications describe the seman-tics and runtime supports for distribution. Successful implementations of solutions such as CORBA, Java Message Service (JMS) or SOAP demonstrate that distributed applications require very different distribution