Document - SoSL: A Service-Oriented Stochastic Logic

2011

Contribution to book Restricted

SoSL: A Service-Oriented Stochastic Logic

De Nicola R., Latella D., Loreti M., Massink M.

Stochastic Logics Stochastic Model Checking

The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous works by the authors for formulating properties of systems specified in StoKlaim, a Markovian extension of Klaim. The main purpose of MoSL is addressing key functional aspects of network aware programming such as distribution awareness, mobility and security and to guarantee their integration with performance and dependability guarantees. In this paper we present SoSL, a variant of MoSL, designed for dealing with specific features of Service-Oriented Computing (SOC). We also show how SoSL formulae can be model-checked against systems descriptions expressed with MarCaSPiS, a process calculus designed for addressing quantitative aspects of SOC. In order to perform actual model checking, we rely on a dedicated front-end that uses existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC).

Source: Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing,, edited by Martin Wirsing, Matthias Hölzl, pp. 447–466. Berlin: Springer-Verlag Berlin, 2011

Publisher: Springer-Verlag Berlin, Berlin, DEU

Metrics

Back to previous page

Cite as

BibTeX entry

@inbook{oai:it.cnr:prodotti:190071,
	title = {SoSL: A Service-Oriented Stochastic Logic},
	author = {De Nicola R. and Latella D. and Loreti M. and Massink M.},
	publisher = {Springer-Verlag Berlin, Berlin, DEU},
	doi = {10.1007/978-3-642-20401-2_21},
	booktitle = {Rigorous Software Engineering for Service-Oriented Systems. Results of the SENSORIA Project on Software Engineering for Service-Oriented Computing,, edited by Martin Wirsing, Matthias Hölzl, pp. 447–466. Berlin: Springer-Verlag Berlin, 2011},
	year = {2011}
}