Towards a logic for performance and mobility (Contributo in atti di convegno)

Type

• Contributo in atti di convegno (Classe)
• Prodotto della ricerca (Classe)

Label

• Towards a logic for performance and mobility (Contributo in atti di convegno) (literal)

Anno

• 2006-01-01T00:00:00+01:00 (literal)

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

• 10.1016/j.entcs.2005.10.037 (literal)

Alternative label

• Rocco De Nicola; Joost-Pieter Katoen; Diego Latella; Mieke Massink (2006)
  Towards a logic for performance and mobility
  in Third Workshop on Quantitative Aspects of Programming Languages (QAPL'05), Edinburgh (UK), April 2-3, 2005
  (literal)

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

• Rocco De Nicola; Joost-Pieter Katoen; Diego Latella; Mieke Massink (literal)

Pagina inizio

• 161 (literal)

Pagina fine

• 175 (literal)

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

• 153 (literal)

Rivista

• Electronic notes in theoretical computer science (Rivista)

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

• 2 (literal)

Note

• Scopu (literal)

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

• Univ. of Firenze, Firenze, Italy; RWTH Aachen, Aachen, Germany, and Univ. of Twente, Enschede, The Netherlands; Istituto di Scienza e Tecnologie dell'Informazione, CNR, Pisa, Italy; Istituto di Scienza e Tecnologie dell'Informazione, CNR, Pisa, Italy (literal)

Titolo

• Towards a logic for performance and mobility (literal)

Abstract

• Klaim is an experimental language designed for modeling and programming distributed systems composed of mobile components where distribution awareness and dynamic system architecture configuration are key issues. StocKlaim [13] is a Markovian extension of the core subset of Klaim which includes process distribution, process mobility, asynchronous communication, and site creation. In this paper, MoSL, a temporal logic for StocKlaim is proposed which addresses and integrates the issues of distribution awareness and mobility and those concerning stochastic behaviour of systems. The satisfiability relation is formally defined over labelled Markov chains. A large fragment of the proposed logic can be translated to action-based CSL for which efficient model-checkers exist. This way, such model-checkers can be used for the verification of StocKlaim models against MoSL properties. An example application is provided in the present paper. (literal)

Editore

• Elsevier (Editore)

Prodotto di

• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)
• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)

Autore CNR

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Insieme di parole chiave

• Keywords of "Towards a logic for performance and mobility" (Insieme di parole chiave)

Incoming links:

Autore CNR di

• MIEKE MASSINK (Unità di personale interno)
• DIEGO LATELLA (Unità di personale interno)

Prodotto

• Istituto di scienza e tecnologie dell'informazione \"Alessandro Faedo\" (ISTI) (Istituto)
• Metodi e Strumenti per la Progettazione di Sistemi Software-Intensive ad Elevata Complessità (ICT.P09.008.002) (Modulo)

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

• Electronic notes in theoretical computer science (Rivista)

Editore di

• Elsevier (Editore)

Insieme di parole chiave di

• Keywords of "Towards a logic for performance and mobility" (Insieme di parole chiave)