Publikation: Mechanical Verification of a Two-Way Sliding Window Protocol
Lade...
Dateien
Zu diesem Dokument gibt es keine Dateien.
Datum
2008
Autor:innen
Herausgeber:innen
ISSN der Zeitschrift
Electronic ISSN
ISBN
Bibliografische Daten
Verlag
Schriftenreihe
Auflagebezeichnung
URI (zitierfähiger Link)
Internationale Patentnummer
Angaben zur Forschungsförderung
Projekt
Open Access-Veröffentlichung
Core Facility der Universität Konstanz
Titel in einer weiteren Sprache
Publikationstyp
Beitrag zu einem Sammelband
Publikationsstatus
Published
Erschienen in
WELCH ., Peter H., ed. and others. Communicating process architectures 2008 : WoTUG- 31. Amsterdam [u.a.]: IOS Press, 2008, pp. 179-203
Zusammenfassung
We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes.We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of μCRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness).
Zusammenfassung in einer weiteren Sprache
Fachgebiet (DDC)
004 Informatik
Schlagwörter
two-way sliding window protocol, specification in μCRL, verification with PVS, a pair of FIFO queues
Konferenz
Rezension
undefined / . - undefined, undefined
Zitieren
ISO 690
BADBAN, Bahareh, Wan FOKKINK, Jaco VAN DE POL, 2008. Mechanical Verification of a Two-Way Sliding Window Protocol. In: WELCH ., Peter H., ed. and others. Communicating process architectures 2008 : WoTUG- 31. Amsterdam [u.a.]: IOS Press, 2008, pp. 179-203BibTex
@incollection{Badban2008Mecha-3058,
year={2008},
title={Mechanical Verification of a Two-Way Sliding Window Protocol},
publisher={IOS Press},
address={Amsterdam [u.a.]},
booktitle={Communicating process architectures 2008 : WoTUG- 31},
pages={179--203},
editor={Welch ., Peter H.},
author={Badban, Bahareh and Fokkink, Wan and van de Pol, Jaco}
}RDF
<rdf:RDF
xmlns:dcterms="http://purl.org/dc/terms/"
xmlns:dc="http://purl.org/dc/elements/1.1/"
xmlns:rdf="http://www.w3.org/1999/02/22-rdf-syntax-ns#"
xmlns:bibo="http://purl.org/ontology/bibo/"
xmlns:dspace="http://digital-repositories.org/ontologies/dspace/0.1.0#"
xmlns:foaf="http://xmlns.com/foaf/0.1/"
xmlns:void="http://rdfs.org/ns/void#"
xmlns:xsd="http://www.w3.org/2001/XMLSchema#" >
<rdf:Description rdf:about="https://kops.uni-konstanz.de/server/rdf/resource/123456789/3058">
<dcterms:rights rdf:resource="https://rightsstatements.org/page/InC/1.0/"/>
<dc:creator>van de Pol, Jaco</dc:creator>
<dc:language>eng</dc:language>
<dc:date rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:59Z</dc:date>
<void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/>
<foaf:homepage rdf:resource="http://localhost:8080/"/>
<dcterms:abstract xml:lang="eng">We prove the correctness of a two-way sliding window protocol with piggybacking, where the acknowledgments of the latest received data are attached to the next data transmitted back into the channel. The window size of both parties are considered to be finite, though they can be of different sizes.We show that this protocol is equivalent (branching bisimilar) to a pair of FIFO queues of finite capacities. The protocol is first modeled and manually proved for its correctness in the process algebraic language of μCRL. We use the theorem prover PVS to formalize and to mechanically prove the correctness. This implies both safety and liveness (under the assumption of fairness).</dcterms:abstract>
<dcterms:issued>2008</dcterms:issued>
<dspace:isPartOfCollection rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dcterms:isPartOf rdf:resource="https://kops.uni-konstanz.de/server/rdf/resource/123456789/36"/>
<dc:creator>Badban, Bahareh</dc:creator>
<dcterms:bibliographicCitation>Publ. in: Communicating process architectures 2008 : WoTUG-31 / ed. by Peter H. Welch ... [et al.]. Amsterdam [u.a.] : IOS Press, 2008, pp. 179-203</dcterms:bibliographicCitation>
<dc:creator>Fokkink, Wan</dc:creator>
<dc:contributor>van de Pol, Jaco</dc:contributor>
<dc:contributor>Fokkink, Wan</dc:contributor>
<dc:contributor>Badban, Bahareh</dc:contributor>
<bibo:uri rdf:resource="http://kops.uni-konstanz.de/handle/123456789/3058"/>
<dc:rights>terms-of-use</dc:rights>
<dcterms:title>Mechanical Verification of a Two-Way Sliding Window Protocol</dcterms:title>
<dcterms:available rdf:datatype="http://www.w3.org/2001/XMLSchema#dateTime">2011-03-23T10:15:59Z</dcterms:available>
</rdf:Description>
</rdf:RDF>
