Mechanical Verification of a Two-Way Sliding Window Protocol


Dateien zu dieser Ressource

Dateien Größe Format Anzeige

Zu diesem Dokument gibt es keine Dateien.

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, pp. 179-203

@incollection{Badban2008Mecha-3058, title={Mechanical Verification of a Two-Way Sliding Window Protocol}, year={2008}, address={Amsterdam [u.a.]}, publisher={IOS Press}, 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 xmlns:dcterms="" xmlns:dc="" xmlns:rdf="" xmlns:bibo="" xmlns:dspace="" xmlns:foaf="" xmlns:void="" xmlns:xsd="" > <rdf:Description rdf:about=""> <dc:contributor>van de Pol, Jaco</dc:contributor> <dcterms:issued>2008</dcterms:issued> <foaf:homepage rdf:resource="http://localhost:8080/jspui"/> <dc:creator>Badban, Bahareh</dc:creator> <dc:language>eng</dc:language> <dc:contributor>Fokkink, Wan</dc:contributor> <dcterms:rights rdf:resource=""/> <dcterms:available rdf:datatype="">2011-03-23T10:15:59Z</dcterms:available> <bibo:uri rdf:resource=""/> <dcterms:isPartOf rdf:resource=""/> <dcterms:title>Mechanical Verification of a Two-Way Sliding Window Protocol</dcterms:title> <dc:creator>Fokkink, Wan</dc:creator> <dc:date rdf:datatype="">2011-03-23T10:15:59Z</dc:date> <dspace:isPartOfCollection rdf:resource=""/> <dc:rights>terms-of-use</dc:rights> <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> <void:sparqlEndpoint rdf:resource="http://localhost/fuseki/dspace/sparql"/> <dc:creator>van de Pol, Jaco</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:contributor>Badban, Bahareh</dc:contributor> </rdf:Description> </rdf:RDF>

Das Dokument erscheint in:

KOPS Suche


Mein Benutzerkonto