Verification of clock synchronization algorithms: experiments on a combination of deductive tools
Identifieur interne : 003C55 ( Istex/Corpus ); précédent : 003C54; suivant : 003C56Verification of clock synchronization algorithms: experiments on a combination of deductive tools
Auteurs : Damián Barsotti ; Leonor Prensa Nieto ; Alwen TiuSource :
- Formal Aspects of Computing [ 0934-5043 ] ; 2007-08-01.
English descriptors
Abstract
Abstract: We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.
Url:
DOI: 10.1007/s00165-007-0027-6
Links to Exploration step
ISTEX:FC6C906EEB26F98AA495952B6296FE5EFF6B018BLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title><author><name sortKey="Barsotti, Damian" sort="Barsotti, Damian" uniqKey="Barsotti D" first="Damián" last="Barsotti">Damián Barsotti</name><affiliation><mods:affiliation>Universidad Nacional de Córdoba, Ciudad Universitaria, 5000, Córdoba, Argentina</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: damian@famaf.unc.edu.ar</mods:affiliation></affiliation></author><author><name sortKey="Nieto, Leonor Prensa" sort="Nieto, Leonor Prensa" uniqKey="Nieto L" first="Leonor Prensa" last="Nieto">Leonor Prensa Nieto</name><affiliation><mods:affiliation>LORIA, 54506, Vandoeuvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Leonor.Prensa@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Tiu, Alwen" sort="Tiu, Alwen" uniqKey="Tiu A" first="Alwen" last="Tiu">Alwen Tiu</name><affiliation><mods:affiliation>Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Alwen.Tiu@anu.edu.au</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FC6C906EEB26F98AA495952B6296FE5EFF6B018B</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/s00165-007-0027-6</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C55</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C55</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title><author><name sortKey="Barsotti, Damian" sort="Barsotti, Damian" uniqKey="Barsotti D" first="Damián" last="Barsotti">Damián Barsotti</name><affiliation><mods:affiliation>Universidad Nacional de Córdoba, Ciudad Universitaria, 5000, Córdoba, Argentina</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: damian@famaf.unc.edu.ar</mods:affiliation></affiliation></author><author><name sortKey="Nieto, Leonor Prensa" sort="Nieto, Leonor Prensa" uniqKey="Nieto L" first="Leonor Prensa" last="Nieto">Leonor Prensa Nieto</name><affiliation><mods:affiliation>LORIA, 54506, Vandoeuvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Leonor.Prensa@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Tiu, Alwen" sort="Tiu, Alwen" uniqKey="Tiu A" first="Alwen" last="Tiu">Alwen Tiu</name><affiliation><mods:affiliation>Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Alwen.Tiu@anu.edu.au</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Formal Aspects of Computing</title><title level="j" type="sub">Applicable Formal Methods</title><title level="j" type="abbrev">Form Asp Comp</title><idno type="ISSN">0934-5043</idno><idno type="eISSN">1433-299X</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>London</pubPlace><date type="published" when="2007-08-01">2007-08-01</date><biblScope unit="volume">19</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="321">321</biblScope><biblScope unit="page" to="341">341</biblScope></imprint><idno type="ISSN">0934-5043</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0934-5043</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Clock synchronization</term><term>Combination of deductive tools</term><term>Theorem proving</term><term>Verification</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.</div></front></TEI><istex><corpusName>springer-journals</corpusName><author><json:item><name>Damián Barsotti</name><affiliations><json:string>Universidad Nacional de Córdoba, Ciudad Universitaria, 5000, Córdoba, Argentina</json:string><json:string>E-mail: damian@famaf.unc.edu.ar</json:string></affiliations></json:item><json:item><name>Leonor Prensa Nieto</name><affiliations><json:string>LORIA, 54506, Vandoeuvre-lès-Nancy, France</json:string><json:string>E-mail: Leonor.Prensa@loria.fr</json:string></affiliations></json:item><json:item><name>Alwen Tiu</name><affiliations><json:string>Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia</json:string><json:string>E-mail: Alwen.Tiu@anu.edu.au</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>Theorem proving</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Verification</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Clock synchronization</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>Combination of deductive tools</value></json:item></subject><articleId><json:string>27</json:string><json:string>s00165-007-0027-6</json:string></articleId><arkIstex>ark:/67375/VQC-SWGG5RH3-X</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.</abstract><qualityIndicators><score>8.56</score><pdfWordCount>9397</pdfWordCount><pdfCharCount>48156</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>21</pdfPageCount><pdfPageSize>595 x 791 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>130</abstractWordCount><abstractCharCount>967</abstractCharCount><keywordCount>4</keywordCount></qualityIndicators><title>Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title><genre><json:string>research-article</json:string></genre><host><title>Formal Aspects of Computing</title><language><json:string>unknown</json:string></language><publicationDate>2007</publicationDate><copyrightDate>2007</copyrightDate><issn><json:string>0934-5043</json:string></issn><eissn><json:string>1433-299X</json:string></eissn><journalId><json:string>165</json:string></journalId><volume>19</volume><issue>3</issue><pages><first>321</first><last>341</last></pages><genre><json:string>journal</json:string></genre><subject><json:item><value>Computational Mathematics and Numerical Analysis</value></json:item><json:item><value>Theory of Computation</value></json:item><json:item><value>Math Applications in Computer Science</value></json:item></subject></host><ark><json:string>ark:/67375/VQC-SWGG5RH3-X</json:string></ark><publicationDate>2007</publicationDate><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/s00165-007-0027-6</json:string></doi><id>FC6C906EEB26F98AA495952B6296FE5EFF6B018B</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">Springer-Verlag</publisher><pubPlace>London</pubPlace><availability><licence><p>British Computer Society, 2007</p></licence><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</p></availability><date>2006-04-07</date></publicationStmt><notesStmt><note type="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note><note type="journal" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note><note>Original Article</note></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title><author xml:id="author-0000"><persName><forename type="first">Damián</forename><surname>Barsotti</surname></persName><email>damian@famaf.unc.edu.ar</email><affiliation>Universidad Nacional de Córdoba, Ciudad Universitaria, 5000, Córdoba, Argentina</affiliation></author><author xml:id="author-0001" corresp="yes"><persName><forename type="first">Leonor</forename><surname>Nieto</surname></persName><email>Leonor.Prensa@loria.fr</email><affiliation>LORIA, 54506, Vandoeuvre-lès-Nancy, France</affiliation></author><author xml:id="author-0002" corresp="yes"><persName><forename type="first">Alwen</forename><surname>Tiu</surname></persName><email>Alwen.Tiu@anu.edu.au</email><affiliation>Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia</affiliation></author><idno type="istex">FC6C906EEB26F98AA495952B6296FE5EFF6B018B</idno><idno type="ark">ark:/67375/VQC-SWGG5RH3-X</idno><idno type="DOI">10.1007/s00165-007-0027-6</idno><idno type="article-id">27</idno><idno type="article-id">s00165-007-0027-6</idno></analytic><monogr><title level="j">Formal Aspects of Computing</title><title level="j" type="sub">Applicable Formal Methods</title><title level="j" type="abbrev">Form Asp Comp</title><idno type="pISSN">0934-5043</idno><idno type="eISSN">1433-299X</idno><idno type="journal-ID">true</idno><idno type="issue-article-count">8</idno><idno type="volume-issue-count">4</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>London</pubPlace><date type="published" when="2007-08-01"></date><biblScope unit="volume">19</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="321">321</biblScope><biblScope unit="page" to="341">341</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2006-04-07</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.</p></abstract><textClass xml:lang="en"><keywords scheme="keyword"><list><head>Keywords</head><item><term>Theorem proving</term></item><item><term>Verification</term></item><item><term>Clock synchronization</term></item><item><term>Combination of deductive tools</term></item></list></keywords></textClass><textClass><keywords scheme="Journal Subject"><list><head>Computer Science</head><item><term>Computational Mathematics and Numerical Analysis</term></item><item><term>Theory of Computation</term></item><item><term>Math Applications in Computer Science</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2006-04-07">Created</change><change when="2007-08-01">Published</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-journals not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer-Verlag</PublisherName><PublisherLocation>London</PublisherLocation></PublisherInfo><Journal OutputMedium="All"><JournalInfo JournalProductType="ArchiveJournal" NumberingStyle="ContentOnly"><JournalID>165</JournalID><JournalPrintISSN>0934-5043</JournalPrintISSN><JournalElectronicISSN>1433-299X</JournalElectronicISSN><JournalTitle>Formal Aspects of Computing</JournalTitle><JournalSubTitle>Applicable Formal Methods</JournalSubTitle><JournalAbbreviatedTitle>Form Asp Comp</JournalAbbreviatedTitle><JournalSubjectGroup><JournalSubject Type="Primary">Computer Science</JournalSubject><JournalSubject Type="Secondary">Computational Mathematics and Numerical Analysis</JournalSubject><JournalSubject Type="Secondary">Theory of Computation </JournalSubject><JournalSubject Type="Secondary">Math Applications in Computer Science </JournalSubject></JournalSubjectGroup></JournalInfo><Volume OutputMedium="All"><VolumeInfo TocLevels="0" VolumeType="Regular"><VolumeIDStart>19</VolumeIDStart><VolumeIDEnd>19</VolumeIDEnd><VolumeIssueCount>4</VolumeIssueCount></VolumeInfo><Issue IssueType="Regular" OutputMedium="All"><IssueInfo TocLevels="0"><IssueIDStart>3</IssueIDStart><IssueIDEnd>3</IssueIDEnd><IssueArticleCount>8</IssueArticleCount><IssueHistory><OnlineDate><Year>2007</Year><Month>7</Month><Day>25</Day></OnlineDate><PrintDate><Year>2007</Year><Month>7</Month><Day>25</Day></PrintDate><CoverDate><Year>2007</Year><Month>8</Month></CoverDate></IssueHistory><IssueCopyright><CopyrightHolderName>British Computer Society</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></IssueCopyright></IssueInfo><Article ID="s00165-007-0027-6" OutputMedium="All"><ArticleInfo ArticleType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="ContentOnly" TocLevels="0"><ArticleID>27</ArticleID><ArticleDOI>10.1007/s00165-007-0027-6</ArticleDOI><ArticleSequenceNumber>4</ArticleSequenceNumber><ArticleTitle Language="En">Verification of clock synchronization algorithms: experiments on a combination of deductive tools</ArticleTitle><ArticleCategory>Original Article</ArticleCategory><ArticleFirstPage>321</ArticleFirstPage><ArticleLastPage>341</ArticleLastPage><ArticleHistory><RegistrationDate><Year>2007</Year><Month>3</Month><Day>8</Day></RegistrationDate><Received><Year>2006</Year><Month>4</Month><Day>7</Day></Received><Revised><Year>2006</Year><Month>8</Month><Day>3</Day></Revised><Accepted><Year>2007</Year><Month>2</Month><Day>12</Day></Accepted><OnlineDate><Year>2007</Year><Month>5</Month><Day>3</Day></OnlineDate></ArticleHistory><ArticleCopyright><CopyrightHolderName>British Computer Society</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></ArticleCopyright><ArticleGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ArticleGrants></ArticleInfo><ArticleHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Damián</GivenName><FamilyName>Barsotti</FamilyName></AuthorName><Contact><Email>damian@famaf.unc.edu.ar</Email></Contact></Author><Author AffiliationIDS="Aff2" CorrespondingAffiliationID="Aff2"><AuthorName DisplayOrder="Western"><GivenName>Leonor</GivenName><GivenName>Prensa</GivenName><FamilyName>Nieto</FamilyName></AuthorName><Contact><Email>Leonor.Prensa@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff3" CorrespondingAffiliationID="Aff3"><AuthorName DisplayOrder="Western"><GivenName>Alwen</GivenName><FamilyName>Tiu</FamilyName></AuthorName><Contact><Email>Alwen.Tiu@anu.edu.au</Email></Contact></Author><Affiliation ID="Aff1"><OrgName>Universidad Nacional de Córdoba, Ciudad Universitaria</OrgName><OrgAddress><Postcode>5000</Postcode><City>Córdoba</City><Country Code="AR">Argentina</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>LORIA</OrgName><OrgAddress><Postcode>54506</Postcode><City>Vandoeuvre-lès-Nancy</City><Country Code="FR">France</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgDivision>Research School of Information Sciences and Engineering</OrgDivision><OrgName>Australian National University and National ICT Australia</OrgName><OrgAddress><City>Canberra</City><State>ACT</State><Postcode>0200</Postcode><Country Code="AU">Australia</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>Theorem proving</Keyword><Keyword>Verification</Keyword><Keyword>Clock synchronization</Keyword><Keyword>Combination of deductive tools</Keyword></KeywordGroup></ArticleHeader><NoBody></NoBody></Article></Issue></Volume></Journal></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Verification of clock synchronization algorithms: experiments on a combination of deductive tools</title></titleInfo><name type="personal"><namePart type="given">Damián</namePart><namePart type="family">Barsotti</namePart><affiliation>Universidad Nacional de Córdoba, Ciudad Universitaria, 5000, Córdoba, Argentina</affiliation><affiliation>E-mail: damian@famaf.unc.edu.ar</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal" displayLabel="corresp"><namePart type="given">Leonor</namePart><namePart type="given">Prensa</namePart><namePart type="family">Nieto</namePart><affiliation>LORIA, 54506, Vandoeuvre-lès-Nancy, France</affiliation><affiliation>E-mail: Leonor.Prensa@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal" displayLabel="corresp"><namePart type="given">Alwen</namePart><namePart type="family">Tiu</namePart><affiliation>Research School of Information Sciences and Engineering, Australian National University and National ICT Australia, 0200, Canberra, ACT, Australia</affiliation><affiliation>E-mail: Alwen.Tiu@anu.edu.au</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre><originInfo><publisher>Springer-Verlag</publisher><place><placeTerm type="text">London</placeTerm></place><dateCreated encoding="w3cdtf">2006-04-07</dateCreated><dateIssued encoding="w3cdtf">2007-08-01</dateIssued><copyrightDate encoding="w3cdtf">2007</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: We report on an experiment in combining the theorem prover Isabelle with automatic first-order arithmetic provers to increase automation on the verification of distributed protocols. As a case study for the experiment we verify several averaging clock synchronization algorithms. We present a formalization of Schneider’s generalized clock synchronization protocol [Sch87] in Isabelle/HOL. Then, we verify that the convergence functions used in two clock synchronization algorithms, namely, the Interactive Convergence Algorithm (ICA) of Lamport and Melliar-Smith [LMS85] and the Fault-tolerant Midpoint algorithm of Lundelius–Lynch [LL84], satisfy Schneider’s general conditions for correctness. The proofs are completely formalized in Isabelle/HOL. We identify parts of the proofs which are not fully automatically proven by Isabelle built-in tactics and show that these proofs can be handled by automatic first-order provers with support for arithmetics.</abstract><note>Original Article</note><subject lang="en"><genre>Keywords</genre><topic>Theorem proving</topic><topic>Verification</topic><topic>Clock synchronization</topic><topic>Combination of deductive tools</topic></subject><relatedItem type="host"><titleInfo><title>Formal Aspects of Computing</title><subTitle>Applicable Formal Methods</subTitle></titleInfo><titleInfo type="abbreviated"><title>Form Asp Comp</title></titleInfo><genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre><originInfo><publisher>Springer</publisher><dateIssued encoding="w3cdtf">2007-07-25</dateIssued><copyrightDate encoding="w3cdtf">2007</copyrightDate></originInfo><subject><genre>Computer Science</genre><topic>Computational Mathematics and Numerical Analysis</topic><topic>Theory of Computation</topic><topic>Math Applications in Computer Science</topic></subject><identifier type="ISSN">0934-5043</identifier><identifier type="eISSN">1433-299X</identifier><identifier type="JournalID">165</identifier><identifier type="IssueArticleCount">8</identifier><identifier type="VolumeIssueCount">4</identifier><part><date>2007</date><detail type="volume"><number>19</number><caption>vol.</caption></detail><detail type="issue"><number>3</number><caption>no.</caption></detail><extent unit="pages"><start>321</start><end>341</end></extent></part><recordInfo><recordOrigin>British Computer Society, 2007</recordOrigin></recordInfo></relatedItem><identifier type="istex">FC6C906EEB26F98AA495952B6296FE5EFF6B018B</identifier><identifier type="ark">ark:/67375/VQC-SWGG5RH3-X</identifier><identifier type="DOI">10.1007/s00165-007-0027-6</identifier><identifier type="ArticleID">27</identifier><identifier type="ArticleID">s00165-007-0027-6</identifier><accessCondition type="use and reproduction" contentType="copyright">British Computer Society, 2007</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-3XSW68JL-F">springer</recordContentSource><recordOrigin>British Computer Society, 2007</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/VQC-SWGG5RH3-X/record.json</uri></json:item></metadata><serie></serie></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 003C55 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003C55 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:FC6C906EEB26F98AA495952B6296FE5EFF6B018B
|texte= Verification of clock synchronization algorithms: experiments on a combination of deductive tools
}}
| This area was generated with Dilib version V0.6.33. |  |