Model checking mobile stochastic logic.

Share/Save/Bookmark

De Nicola, Rocco and Katoen, Joost-Pieter and Latella, Diego and Loreti, Michele and Massink, Mieke (2007) Model checking mobile stochastic logic. Theoretical Computer Science, 382 (1). pp. 42-70. ISSN 0304-3975

[img]PDF
Restricted to UT campus only
: Request a copy
585Kb
Abstract: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.
Item Type:Article
Copyright:© 2007 Elsevier
Faculty:
Electrical Engineering, Mathematics and Computer Science (EEMCS)
Research Group:
Link to this item:http://purl.utwente.nl/publications/62049
Official URL:http://dx.doi.org/10.1016/j.tcs.2007.05.008
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page

Metis ID: 245850