InforLorV4, Main, Merge, bibRecord, 008D86

Incremental proof of the producer/consumer property for the PCI protocol

Identifieur interne : 008D86 ( Main/Merge ); précédent : 008D85; suivant : 008D87

Incremental proof of the producer/consumer property for the PCI protocol

Auteurs : Dominique Cansell [France] ; Ganesh Gopalakrishnan [États-Unis] ; Mike Jones [États-Unis] ; Dominique Méry [France] ; Airy Weinzoepflen [France]

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2002.

RBID : Pascal:02-0202115

Descripteurs français

Pascal (Inist)
- Spécification formelle, Protocole transmission, Méthode raffinement, Démonstration théorème, Vérification programme.

English descriptors

KwdEn :
- Formal specification, Program verification, Refinement method, Theorem proving, Transmission protocol.

Abstract

We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13,15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000881
to stream PascalFrancis, to step Curation: 000171
to stream PascalFrancis, to step Checkpoint: 000801

Links to Exploration step

Pascal:02-0202115

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Incremental proof of the producer/consumer property for the PCI protocol</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
<affiliation wicri:level="2"><inist:fA14 i1="02"><s1>University of Utah</s1>
<s2>Salt Lake City, Utah</s2>
<s3>USA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
<affiliation wicri:level="2"><inist:fA14 i1="03"><s1>Presently at Brigham Young University</s1>
<s2>Provo, Utah</s2>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0202115</idno>
<date when="2002">2002</date>
<idno type="stanalyst">PASCAL 02-0202115 INIST</idno>
<idno type="RBID">Pascal:02-0202115</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000881</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000171</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000801</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000801</idno>
<idno type="wicri:doubleKey">0302-9743:2002:Cansell D:incremental:proof:of</idno>
<idno type="wicri:Area/Main/Merge">008D86</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Incremental proof of the producer/consumer property for the PCI protocol</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
<affiliation wicri:level="2"><inist:fA14 i1="02"><s1>University of Utah</s1>
<s2>Salt Lake City, Utah</s2>
<s3>USA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
<affiliation wicri:level="2"><inist:fA14 i1="03"><s1>Presently at Brigham Young University</s1>
<s2>Provo, Utah</s2>
<s3>USA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>États-Unis</country>
<placeName><region type="state">Utah</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>4 aut.</sZ>
<sZ>5 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2002">2002</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Formal specification</term>
<term>Program verification</term>
<term>Refinement method</term>
<term>Theorem proving</term>
<term>Transmission protocol</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Spécification formelle</term>
<term>Protocole transmission</term>
<term>Méthode raffinement</term>
<term>Démonstration théorème</term>
<term>Vérification programme</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We present an incremental proof of the producer/consumer property for the PCI protocol. In the incremental proof, a corrected model of the multi-bus PCI 2.1 protocol is shown to be a refinement of the producer/consumer property. Multi-bus PCI must be corrected because the original PCI specification violates the producer/consumer property. The final model of PCI includes transaction types and reordering along with the completion mechanism for delayed PCI transactions. Verification results include multiple concurrent sessions of the producer/consumer property in a family of topologically isomorphic network configurations. The remaining configurations are identified and left for future work. In contrast to previous case studies involving this problem [13,15], the incremental proof provides structure which simplifies otherwise difficult monolithic proof attempts.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>États-Unis</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Utah</li>
</region>
<settlement><li>Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
</region>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<name sortKey="Weinzoepflen, Airy" sort="Weinzoepflen, Airy" uniqKey="Weinzoepflen A" first="Airy" last="Weinzoepflen">Airy Weinzoepflen</name>
</country>
<country name="États-Unis"><region name="Utah"><name sortKey="Gopalakrishnan, Ganesh" sort="Gopalakrishnan, Ganesh" uniqKey="Gopalakrishnan G" first="Ganesh" last="Gopalakrishnan">Ganesh Gopalakrishnan</name>
</region>
<name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name>
</country>
</tree>
</affiliations>
</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 008D86 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 008D86 | 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é=     Pascal:02-0202115
   |texte=   Incremental proof of the producer/consumer property for the PCI protocol
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

Incremental proof of the producer/consumer property for the PCI protocol

Incremental proof of the producer/consumer property for the PCI protocol

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri