Incremental Proof of the Producer/Consumer Property for the PCI Protocol
Identifieur interne : 008794 ( Main/Curation ); précédent : 008793; suivant : 008795Incremental 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 ]
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
Abstract
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.
Url:
DOI: 10.1007/3-540-45648-1_2
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :003726
- to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :003683
- to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :001C30
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :008C50
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000881
- to stream PascalFrancis, to step Curation: Pour aller vers cette notice dans l'étape Curation :000171
- to stream PascalFrancis, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :000801
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :008D86
Links to Exploration step
ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">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><country>France</country><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></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><country>France</country><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></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45648-1_2</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VVP7FG8X-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003726</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003726</idno><idno type="wicri:Area/Istex/Curation">003683</idno><idno type="wicri:Area/Istex/Checkpoint">001C30</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C30</idno><idno type="wicri:doubleKey">0302-9743:2002:Cansell D:incremental:proof:of</idno><idno type="wicri:Area/Main/Merge">008C50</idno><idno type="wicri:source">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><idno type="wicri:Area/Main/Curation">008794</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">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"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><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><affiliation wicri:level="1"><country wicri:rule="url">France</country><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"><country xml:lang="fr">États-Unis</country><wicri:regionArea>University of Utah, Salt Lake City, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>presently at Brigham Young University, Provo, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><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><affiliation wicri:level="1"><country wicri:rule="url">France</country><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"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><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>Démonstration théorème</term><term>Méthode raffinement</term><term>Protocole transmission</term><term>Spécification formelle</term><term>Vérification programme</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI><double idat="0302-9743:2002:Cansell D:incremental:proof:of"><INIST><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></INIST><ISTEX><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">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><country>France</country><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></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><country>France</country><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></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421</idno><date when="2002" year="2002">2002</date><idno type="doi">10.1007/3-540-45648-1_2</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-VVP7FG8X-1/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003726</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003726</idno><idno type="wicri:Area/Istex/Curation">003683</idno><idno type="wicri:Area/Istex/Checkpoint">001C30</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001C30</idno><idno type="wicri:doubleKey">0302-9743:2002:Cansell D:incremental:proof:of</idno><idno type="wicri:Area/Main/Merge">008C50</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">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"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><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><affiliation wicri:level="1"><country wicri:rule="url">France</country><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"><country xml:lang="fr">États-Unis</country><wicri:regionArea>University of Utah, Salt Lake City, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Jones, Mike" sort="Jones, Mike" uniqKey="Jones M" first="Mike" last="Jones">Mike Jones</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><wicri:regionArea>presently at Brigham Young University, Provo, Utah</wicri:regionArea><placeName><region type="state">Utah</region></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">États-Unis</country></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation wicri:level="3"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><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><affiliation wicri:level="1"><country wicri:rule="url">France</country><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"><country xml:lang="fr">France</country><wicri:regionArea>LORIA, Nancy</wicri:regionArea><placeName><region type="region">Grand Est</region><region type="old region">Lorraine (région)</region><settlement type="city">Nancy</settlement></placeName></affiliation><affiliation wicri:level="1"><country wicri:rule="url">France</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">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.</div></front></TEI></ISTEX></double></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 008794 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 008794 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Curation
|type= RBID
|clé= ISTEX:E621210A3538DB1E250A1A09F796F0A4511A6421
|texte= Incremental Proof of the Producer/Consumer Property for the PCI Protocol
}}
| This area was generated with Dilib version V0.6.33. |  |