Compositional Verification of Middleware-Based Software Architecture Descriptions

In this paper we present a compositional reasoning to verify middleware-based software architecture descrip-tions. We consider a nowadays typical software system de-velopment, namely the development of a software applica-tion A on a middleware M. Our goal is to efficiently in-tegrate verification techniques, like model checking, in the software life cycle in order to improve the overall software quality. The approach exploits the structure imposed on the system by the software architecture in order to develop an assume-guarantee methodology to reduce properties verifi-cation from global to local. We apply the methodology on a non-trivial case study namely the development of a Gnutella system on top of the SIENA event-notification middleware. 1