Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
Identifieur interne : 007E09 ( Main/Merge ); précédent : 007E08; suivant : 007E10Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
Auteurs : Michaël Rusinowitch [France] ; Sorin Stratulat [France] ; Francis Klay [France]Source :
- Journal of Automated Reasoning [ 0168-7433 ] ; 2003-02-01.
English descriptors
Abstract
Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.
Url:
DOI: 10.1023/A:1023251327012
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 001D20
- to stream Istex, to step Curation: 001C99
- to stream Istex, to step Checkpoint: 001A20
Links to Exploration step
ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name></author><author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name></author><author><name sortKey="Klay, Francis" sort="Klay, Francis" uniqKey="Klay F" first="Francis" last="Klay">Francis Klay</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76</idno><date when="2003" year="2003">2003</date><idno type="doi">10.1023/A:1023251327012</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-P5HVP0B2-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">001D20</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">001D20</idno><idno type="wicri:Area/Istex/Curation">001C99</idno><idno type="wicri:Area/Istex/Checkpoint">001A20</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001A20</idno><idno type="wicri:doubleKey">0168-7433:2003:Rusinowitch M:mechanical:verification:of</idno><idno type="wicri:Area/Main/Merge">007E09</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm</title><author><name sortKey="Rusinowitch, Michael" sort="Rusinowitch, Michael" uniqKey="Rusinowitch M" first="Michaël" last="Rusinowitch">Michaël Rusinowitch</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA-INRIA, 54506, Vandœuvre-les-Nancy Cedex</wicri:regionArea><placeName><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region><settlement type="city">Vandœuvre-lès-Nancy</settlement></placeName></affiliation></author><author><name sortKey="Stratulat, Sorin" sort="Stratulat, Sorin" uniqKey="Stratulat S" first="Sorin" last="Stratulat">Sorin Stratulat</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>INRIA–Sophia Antipolis, 2004 Route des Lucioles, 06092, Sophia Antipolis</wicri:regionArea><placeName><region type="region" nuts="2">Provence-Alpes-Côte d'Azur</region><settlement type="city">Sophia Antipolis</settlement></placeName></affiliation></author><author><name sortKey="Klay, Francis" sort="Klay, Francis" uniqKey="Klay F" first="Francis" last="Klay">Francis Klay</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>Technopole Anticipa, France Telecom CNET DTL/MSV, 2 av. Pierre Marzin, 22307, Lannion</wicri:regionArea><placeName><region type="region" nuts="2">Région Bretagne</region><settlement type="city">Lannion</settlement></placeName></affiliation></author></analytic><monogr></monogr><series><title level="j">Journal of Automated Reasoning</title><title level="j" type="abbrev">Journal of Automated Reasoning</title><idno type="ISSN">0168-7433</idno><idno type="eISSN">1573-0670</idno><imprint><publisher>Kluwer Academic Publishers</publisher><pubPlace>Dordrecht</pubPlace><date type="published" when="2003-02-01">2003-02-01</date><biblScope unit="volume">30</biblScope><biblScope unit="issue">2</biblScope><biblScope unit="page" from="153">153</biblScope><biblScope unit="page" to="177">177</biblScope></imprint><idno type="ISSN">0168-7433</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0168-7433</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>ABR conformance algorithm</term><term>PVS theorem prover</term><term>mechanical verification</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: The Available Bit Rate protocol (ABR) for ATM networks is well adapted to data traffic by providing minimum rate guarantees and low cell loss to the ABR source end system. An ABR conformance algorithm for controlling the source rates through an interface has been defined by ATM Forum, and a more efficient version of it has been designed by Rabadan and Klay. We present in this work the first complete mechanical verification of the equivalence between these two algorithms. The proof is involved and has been supported by the PVS theorem prover. It has required many lemmas, case analysis, and induction reasoning for the manipulation of unbounded scheduling lists. Some ABR conformance protocols have been verified in previous works. However, these protocols are approximations of the one we consider here. In particular, the algorithms assume a bound on the number of rates to be scheduled.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Merge
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 007E09 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 007E09 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Merge
|type= RBID
|clé= ISTEX:7D3A15E739ABB9074DA25DB14FF8816664BC9D76
|texte= Mechanical Verification of an Ideal Incremental ABR Conformance Algorithm
}}
| This area was generated with Dilib version V0.6.33. |  |