PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Katoen J., Latella D., Loreti M., Massink M. Model checking mobile stochastic logic. In: Theoretical Computer Science, vol. 382 (1) pp. 42 - 70. Quantitative Aspects of Programming Languages. A. Di Pierro and H. Wiklicky (eds.). Elsevier, 2007.
 
 
Abstract
(English)
The Temporal Mobile Stochastic Logic (MoSL) has been introduced in previous work by the authors for formulating properties of systems specified in StoKLAIM, a Markovian extension of KLAIM. The main purpose of MoSL is to address key functional aspects of global computing such as distribution awareness, mobility, and security and their integration with performance and dependability guarantees. In this paper we present MoSL+, an extension of MoSL, which incorporates some basic features of the Modal Logic for MObility MoMo, a logic specifically designed for dealing with resource management and mobility aspects of concurrent behaviours. We also show how MoSL+ formulae can be model-checked against StoKLAIM specifications. For this purpose we show how existing state-based stochastic model-checkers, like e.g. the Markov Reward Model Checker (MRMC), can be exploited by using a front-end for StoKLAIM that performs appropriate pre-processing of MoSL+ formulae. The proposed approach is illustrated by modelling and verifying a sample system.
URL: http://dx.doi.org/10.1016/j.tcs.2007.05.008
Subject Concurrency Theory
Formal Methods
Model Checking
Service-Oriented Computing
Stochastic Temporal Logic
D.2.4 Software/Program Verification
F.4.1 Mathematical Logic
68N30 Mathematical Aspects of Software Engineering


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