Model checking groupware protocols (Contributo in volume (capitolo o saggio))

Type
Label
  • Model checking groupware protocols (Contributo in volume (capitolo o saggio)) (literal)
Anno
  • 2004-01-01T00:00:00+01:00 (literal)
Alternative label
  • Ter Beek M. H.; Massink M.; Latella D.; Gnesi S. (2004)
    Model checking groupware protocols
    IOS Press, Amsterdam (Paesi Bassi) in Cooperative Systems Design - Scenario-Based Design of Collaborative Systems, 2004
    (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#autori
  • Ter Beek M. H.; Massink M.; Latella D.; Gnesi S. (literal)
Pagina inizio
  • 179 (literal)
Pagina fine
  • 194 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#citta
  • Amsterdam (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#titoloVolume
  • Cooperative Systems Design - Scenario-Based Design of Collaborative Systems (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#volumeInCollana
  • 107 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#affiliazioni
  • ISTI-CNR, Pisa, Italy (literal)
Titolo
  • Model checking groupware protocols (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#inCollana
  • Cooperative Systems Design - Scenario-Based Design of Collaborative Systems (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#isbn
  • 978-1586034221 (literal)
Http://www.cnr.it/ontology/cnr/pubblicazioni.owl#curatoriVolume
  • F. Darses; R. Dieng; C. Simone; M. Zacklad (literal)
Abstract
  • The enormous improvements in the efficiency of model-checking techniques in recent years facilitates their application to ever more complex systems of concurrent and distributed nature. Many of the protocols underlying groupware systems need to deal with those aspects as well, which makes them notoriously hard to analyse on paper or by traditional means such as testing and simulation. Model checking allows for the automatic analysis of correctness and liveness properties in an exhaustive and time-efficient way, generating counterexamples in case certain properties are found not to be satisfied. In this paper we show how model checking can be used for the verification of protocols underlying groupware systems. To this aim, we present a case study of those protocols underlying the Clock toolkit [GUN96,UG99] that are responsible for its network communication, concurrency control, and distributed notification aspects. In particular, we address key issues related to concurrency control, data consistency, view consistency, and absence of (user) starvation. As a result, we contribute to the verification of Clock's underlying groupware protocols, which was attempted in [Urn98] with very limited success. (literal)
Editore
Prodotto di
Autore CNR

Incoming links:


Autore CNR di
Prodotto
Editore di
data.CNR.it