The publish-subscribe architectural style has recently emerged as a promising approach to tackle the dynamism of modern distributed applications. The correctness of these applications does not only depend on the behavior of each component in isolation, but the interactions among components and the delivery infrastructure play key roles. This paper presents the first results on considering the validation of these applications in a probabilistic setting. We use probabilistic model checking techniques on stochastic models to tackle the uncertainty that is embedded in these systems. The communication infrastructure (i.e., the transmission channels and the publish-subscribe middleware) are modeled directly by means of probabilistic timed automata. Application components are modeled by using statechart diagrams and then translated into probabilistic timed automata. The main elements of the approach are described through an example.

Formal analysis of Publish-Subscribe systems by probabilistic timed automata

SPOLETINI, PAOLA
2007-01-01

Abstract

The publish-subscribe architectural style has recently emerged as a promising approach to tackle the dynamism of modern distributed applications. The correctness of these applications does not only depend on the behavior of each component in isolation, but the interactions among components and the delivery infrastructure play key roles. This paper presents the first results on considering the validation of these applications in a probabilistic setting. We use probabilistic model checking techniques on stochastic models to tackle the uncertainty that is embedded in these systems. The communication infrastructure (i.e., the transmission channels and the publish-subscribe middleware) are modeled directly by means of probabilistic timed automata. Application components are modeled by using statechart diagrams and then translated into probabilistic timed automata. The main elements of the approach are described through an example.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11383/1682816
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact