Timed Automata Modeling and Verification for Publish-Subscribe Structures Using Distributed Resources

摘要

In this paper we present a Timed Automata model for the Publish/Subscribe paradigm in the context of Web Service Compositions with distributed resources, on the basis of an algebraic language inspired by the WSRF standard constructions. This framework allows a set of participants in a Web Service composition to interact with one another and also to manage a collection of distributed resources. The model includes operations for clients to publish, discover and subscribe to resources, so as to be notified when the resource property values fulfill certain conditions (topic-based subscription). Simulation and model-checking techniques can therefore be applied to the obtained network of timed automata, in order to check whether certain properties of interest are satisfied. A specific case study is finally presented to illustrate the model and the verification of the relevant properties on the obtained timed automata model.