Model-checking verification of publish-subscribe architectures in web service contexts
Gregorio Dı́az, M. Emilia Cambronero, Hermenegilda Macià, Valentín Valero · 2015
In this paper we consider a Timed Automata model for the Publish/Subscribe paradigm, where special attention is given to its temporal aspects. Despite this special interest, we present a generic model for publishing and managing WS-resourses in the context of Web services with distributed resources. The model includes operations for clients to discover and subscribe to resources, with the intention of being notified when the resource property values fulfill certain conditions. Furthermore, error handling is provided in case discovery fails or a resource life has expired. Model-checking is used to verify the model soundness, by means of the UPPAAL tool, and a specific case study is presented to illustrate how the model deals with the scalability problem.