Deductive Verification of Distributed Groupware Systems
Identifieur interne : 003E84 ( Crin/Curation ); précédent : 003E83; suivant : 003E85Deductive Verification of Distributed Groupware Systems
Auteurs : Abdessamad Imine ; Pascal Molli ; Gérald Oster ; Michaël RusinowitchSource :
English descriptors
- KwdEn :
Abstract
Replication-based distributed systems consist of a group of users manipulating a shared object (like a text document, a filesystem, ...). Operational Transformation (OT) algorithms are applied for achieving convergence in these systems. However, the design of such algorithms is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show that many OT algorithms in the litterature do no satisfy convergence properties unlike stated by their authors.
Links toward previous steps (curation, corpus...)
- to stream Crin, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003E84
Links to Exploration step
CRIN:imine04aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="97">Deductive Verification of Distributed Groupware Systems</title></titleStmt><publicationStmt><idno type="RBID">CRIN:imine04a</idno><date when="2004" year="2004">2004</date><idno type="wicri:Area/Crin/Corpus">003E84</idno><idno type="wicri:Area/Crin/Curation">003E84</idno><idno type="wicri:explorRef" wicri:stream="Crin" wicri:step="Curation">003E84</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Deductive Verification of Distributed Groupware Systems</title><author><name sortKey="Imine, Abdessamad" sort="Imine, Abdessamad" uniqKey="Imine A" first="Abdessamad" last="Imine">Abdessamad Imine</name></author><author><name sortKey="Molli, Pascal" sort="Molli, Pascal" uniqKey="Molli P" first="Pascal" last="Molli">Pascal Molli</name></author><author><name sortKey="Oster, Gerald" sort="Oster, Gerald" uniqKey="Oster G" first="Gérald" last="Oster">Gérald Oster</name></author><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>algebraic specification</term><term>distributed systems</term><term>formal verification</term><term>operational transformation</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2255">Replication-based distributed systems consist of a group of users manipulating a shared object (like a text document, a filesystem, ...). Operational Transformation (OT) algorithms are applied for achieving convergence in these systems. However, the design of such algorithms is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show that many OT algorithms in the litterature do no satisfy convergence properties unlike stated by their authors.</div></front></TEI><BibTex type="inproceedings"><ref>imine04a</ref><crinnumber>A04-R-187</crinnumber><category>3</category><equipe>CASSIS</equipe><author><e>Imine, Abdessamad</e><e>Molli, Pascal</e><e>Oster, Gérald</e><e>Rusinowitch, Michaël</e></author><title>Deductive Verification of Distributed Groupware Systems</title><booktitle>{Tenth International Conference on Algebraic Methodology and Software Technology - AMAST 2004, Stirling, Scotland, United Kingdom}</booktitle><year>2004</year><editor>Charles Rattray and Savitri Maharaj and Carron Shankland</editor><volume>3116</volume><series>Lecture Notes in Computer Science</series><pages>226-240</pages><month>Jul</month><publisher>Springer</publisher><keywords><e>algebraic specification</e><e>formal verification</e><e>distributed systems</e><e>operational transformation</e></keywords><abstract>Replication-based distributed systems consist of a group of users manipulating a shared object (like a text document, a filesystem, ...). Operational Transformation (OT) algorithms are applied for achieving convergence in these systems. However, the design of such algorithms is a difficult and error-prone activity, since building the correct operations for maintaining good convergence properties of the local copies requires examining a large number of situations. In this paper, we present the modelling and deductive verification of OT algorithms with algebraic specifications. We show that many OT algorithms in the litterature do no satisfy convergence properties unlike stated by their authors.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003E84 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Curation/biblio.hfd -nk 003E84 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Curation
|type= RBID
|clé= CRIN:imine04a
|texte= Deductive Verification of Distributed Groupware Systems
}}
| This area was generated with Dilib version V0.6.33. |  |