PUMA
Istituto di Scienza e Tecnologie dell'Informazione     
De Nicola R., Katoen J., Latella D., Loreti M., Massink M. MoSL: A Stochastic Logic for StoKLAIM. Technical report, 2006.
 
 
Abstract
(English)
The programming and modeling language KLAIM has been designed to address key functional aspects of global computing such as distribution awareness, (code and agent) mobility, and privacy aspects. This paper concentrates on their integration with performance and dependability aspects, the logical characterization of performance and dependability requirements, and the automatic validation of system models against integrated formal functional and performance/dependability requirements. To that purpose the temporal logic MoSL is introduced for formulating properties of models specified in StoKLAIM, a Markovian extension of KLAIM introduced in previous work of the authors. MoSL is inspired by (an action-based version of) CSL, an extension of CTL with ample means to refer to performance and dependability aspects. It is shown that a substantial fragment of the logic can be mapped onto the input language of existing probabilistic model checkers, thus allowing for the automated verification of qualitative and quantitative properties of network-aware programs. The approach is illustrated by modeling and verifying the spreading of a virus through a network.
Subject Stochastic Logics
Temporal Logics
Spatial Logics
Timed Logics
Stochastic Model Checking
D.2.4 Software/Program Verification
60J99 Markov processes
68R99 Discrete mathematics in relation to computer science


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