Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Latella D., Loreti M., Massink M. SoSL: a Service-oriented Stochastic Logic. Martin Wirsing, Matthias Hölzl (eds.). (Lecture Notes in Computer Science, vol. 6582). Berlin: Springer, 2011.
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).
URL: http://www.springerlink.com/content/h6223l787963l534/
DOI: 10.1007/978-3-642-20401-2_21
Subject Stochastic Logics
Stochastic Model Checking
H.1 Models and Principles
F.4 Mathematical Logic and Formal Languages
68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Icona documento 1) Download Document PDF

Icona documento Open access Icona documento Restricted Icona documento Private


Per ulteriori informazioni, contattare: Librarian http://puma.isti.cnr.it

Valid HTML 4.0 Transitional