http://www.cnr.it/ontology/cnr/individuo/prodotto/ID160329

MoSL: A Stochastic Logic for StoKLAIM (Rapporti tecnici, manuali, carte geologiche e tematiche e prodotti multimediali)

Type

Label

MoSL: A Stochastic Logic for StoKLAIM (Rapporti tecnici, manuali, carte geologiche e tematiche e prodotti multimediali) (literal)

Anno

Alternative label

De Nicola R.; Katoen J.; Latella D.; Loreti M.; Massink M. (2006)
MoSL: A Stochastic Logic for StoKLAIM
(literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#note

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#descrizioneSinteticaDelProdotto

ABSTRACT: 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. (literal)

Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#supporto