Time Constraint Patterns for Event B Development
Identifieur interne : 003015 ( Istex/Corpus ); précédent : 003014; suivant : 003016Time Constraint Patterns for Event B Development
Auteurs : Dominique Cansell ; Dominique Méry ; Joris RehmSource :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.
Url:
DOI: 10.1007/11955757_13
Links to Exploration step
ISTEX:CAF1976E06FD7349E71DF25222E083D51C33A992Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Time Constraint Patterns for Event B Development</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation><mods:affiliation>Université de Metz, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: cansell@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>Université Henri Poincaré Nancy 1, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rehm, Joris" sort="Rehm, Joris" uniqKey="Rehm J" first="Joris" last="Rehm">Joris Rehm</name><affiliation><mods:affiliation>Université Henri Poincaré Nancy 1, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rehm@loria.fr</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:CAF1976E06FD7349E71DF25222E083D51C33A992</idno><date when="2006" year="2006">2006</date><idno type="doi">10.1007/11955757_13</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003015</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003015</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Time Constraint Patterns for Event B Development</title><author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name><affiliation><mods:affiliation>Université de Metz, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: cansell@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Méry">Dominique Méry</name><affiliation><mods:affiliation>Université Henri Poincaré Nancy 1, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: mery@loria.fr</mods:affiliation></affiliation></author><author><name sortKey="Rehm, Joris" sort="Rehm, Joris" uniqKey="Rehm J" first="Joris" last="Rehm">Joris Rehm</name><affiliation><mods:affiliation>Université Henri Poincaré Nancy 1, </mods:affiliation></affiliation><affiliation><mods:affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: rehm@loria.fr</mods:affiliation></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="eISSN">1611-3349</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: Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.</div></front></TEI><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Dominique Cansell</name><affiliations><json:string>Université de Metz,</json:string><json:string>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</json:string><json:string>E-mail: cansell@loria.fr</json:string></affiliations></json:item><json:item><name>Dominique Méry</name><affiliations><json:string>Université Henri Poincaré Nancy 1,</json:string><json:string>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</json:string><json:string>E-mail: mery@loria.fr</json:string></affiliations></json:item><json:item><name>Joris Rehm</name><affiliations><json:string>Université Henri Poincaré Nancy 1,</json:string><json:string>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</json:string><json:string>E-mail: rehm@loria.fr</json:string></affiliations></json:item></author><subject><json:item><lang><json:string>eng</json:string></lang><value>event B</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>pattern</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>distributed systems</value></json:item><json:item><lang><json:string>eng</json:string></lang><value>refinement</value></json:item></subject><arkIstex>ark:/67375/HCB-03FPWSX2-3</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.</abstract><qualityIndicators><refBibsNative>false</refBibsNative><abstractWordCount>109</abstractWordCount><abstractCharCount>685</abstractCharCount><keywordCount>4</keywordCount><score>8.308</score><pdfWordCount>5389</pdfWordCount><pdfCharCount>27748</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>15</pdfPageCount><pdfPageSize>430 x 660 pts</pdfPageSize></qualityIndicators><title>Time Constraint Patterns for Event B Development</title><chapterId><json:string>13</json:string><json:string>Chap13</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>2006</copyrightDate><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><editor><json:item><name>David Hutchison</name><affiliations><json:string>Lancaster University, UK</json:string></affiliations></json:item><json:item><name>Takeo Kanade</name><affiliations><json:string>Carnegie Mellon University, Pittsburgh, PA, USA</json:string></affiliations></json:item><json:item><name>Josef Kittler</name><affiliations><json:string>University of Surrey, Guildford, UK</json:string></affiliations></json:item><json:item><name>Jon M. Kleinberg</name><affiliations><json:string>Cornell University, Ithaca, NY, USA</json:string></affiliations></json:item><json:item><name>Friedemann Mattern</name><affiliations><json:string>ETH Zurich, Switzerland</json:string></affiliations></json:item><json:item><name>John C. Mitchell</name><affiliations><json:string>Stanford University, CA, USA</json:string></affiliations></json:item><json:item><name>Moni Naor</name><affiliations><json:string>Weizmann Institute of Science, Rehovot, Israel</json:string></affiliations></json:item><json:item><name>Oscar Nierstrasz</name><affiliations><json:string>University of Bern, Switzerland</json:string></affiliations></json:item><json:item><name>C. Pandu Rangan</name><affiliations><json:string>Indian Institute of Technology, Madras, India</json:string></affiliations></json:item><json:item><name>Bernhard Steffen</name><affiliations><json:string>University of Dortmund, Germany</json:string></affiliations></json:item><json:item><name>Madhu Sudan</name><affiliations><json:string>Massachusetts Institute of Technology, MA, USA</json:string></affiliations></json:item><json:item><name>Demetri Terzopoulos</name><affiliations><json:string>University of California, Los Angeles, CA, USA</json:string></affiliations></json:item><json:item><name>Dough Tygar</name><affiliations><json:string>University of California, Berkeley, CA, USA</json:string></affiliations></json:item><json:item><name>Moshe Y. Vardi</name><affiliations><json:string>Rice University, Houston, TX, USA</json:string></affiliations></json:item><json:item><name>Gerhard Weikum</name><affiliations><json:string>Max-Planck Institute of Computer Science, Saarbruecken, Germany</json:string></affiliations></json:item></editor></serie><host><title>B 2007: Formal Specification and Development in B</title><language><json:string>unknown</json:string></language><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11955757</json:string></doi><issn><json:string>0302-9743</json:string></issn><eissn><json:string>1611-3349</json:string></eissn><eisbn><json:string>978-3-540-68761-0</json:string></eisbn><bookId><json:string>978-3-540-68761-0</json:string></bookId><isbn><json:string>978-3-540-68760-3</json:string></isbn><volume>4355</volume><pages><first>140</first><last>154</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Jacques Julliand</name><affiliations><json:string>LIFC, Université de Franche-Comté, 16, route de Gray, F-25030, Besançon Cedex, France</json:string><json:string>E-mail: julliand@lifc.univ-fcomte.fr</json:string></affiliations></json:item><json:item><name>Olga Kouchnarenko</name><affiliations><json:string>LIFC – TFC Team, 16 route de Gray, F-25030, Besançon</json:string><json:string>E-mail: Olga.Kouchnarenko@lifc.univ-fcomte.fr</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Software Engineering</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-03FPWSX2-3</json:string></ark><publicationDate>2006</publicationDate><copyrightDate>2006</copyrightDate><doi><json:string>10.1007/11955757_13</json:string></doi><id>CAF1976E06FD7349E71DF25222E083D51C33A992</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Time Constraint Patterns for Event B Development</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="2006">2006</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Time Constraint Patterns for Event B Development</title><author><persName><forename type="first">Dominique</forename><surname>Cansell</surname></persName><email>cansell@loria.fr</email><affiliation><orgName type="institution">Université de Metz</orgName><address><country key=""></country></address></affiliation><affiliation><orgName type="institution">LORIA</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandœvre-lès-Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Dominique</forename><surname>Méry</surname></persName><email>mery@loria.fr</email><affiliation><orgName type="institution">Université Henri Poincaré Nancy 1</orgName><address><country key=""></country></address></affiliation><affiliation><orgName type="institution">LORIA</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandœvre-lès-Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><author><persName><forename type="first">Joris</forename><surname>Rehm</surname></persName><email>rehm@loria.fr</email><affiliation><orgName type="institution">Université Henri Poincaré Nancy 1</orgName><address><country key=""></country></address></affiliation><affiliation><orgName type="institution">LORIA</orgName><address><postBox>BP 239</postBox><postCode>54506</postCode><settlement>Vandœvre-lès-Nancy</settlement><country key="FR">FRANCE</country></address></affiliation></author><idno type="istex">CAF1976E06FD7349E71DF25222E083D51C33A992</idno><idno type="ark">ark:/67375/HCB-03FPWSX2-3</idno><idno type="DOI">10.1007/11955757_13</idno></analytic><monogr><title level="m" type="main">B 2007: Formal Specification and Development in B</title><title level="m" type="sub">7th International Conference of B Users, Besançon, France, January 17-19, 2007. Proceedings</title><title level="m" type="part">Regular Papers</title><idno type="DOI">10.1007/11955757</idno><idno type="book-id">978-3-540-68761-0</idno><idno type="ISBN">978-3-540-68760-3</idno><idno type="eISBN">978-3-540-68761-0</idno><idno type="chapter-id">Chap13</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Jacques</forename><surname>Julliand</surname></persName><email>julliand@lifc.univ-fcomte.fr</email><affiliation><orgName type="department">LIFC</orgName><orgName type="institution">Université de Franche-Comté</orgName><address><street>16, route de Gray</street><postCode>F-25030</postCode><settlement>Besançon Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></editor><editor><persName><forename type="first">Olga</forename><surname>Kouchnarenko</surname></persName><email>Olga.Kouchnarenko@lifc.univ-fcomte.fr</email><affiliation><orgName type="institution">LIFC – TFC Team</orgName><address><street>16 route de Gray</street><postCode>F-25030</postCode><settlement>Besançon</settlement></address></affiliation></editor><imprint><biblScope unit="vol">4355</biblScope><biblScope unit="page" from="140">140</biblScope><biblScope unit="page" to="154">154</biblScope><biblScope unit="chapter-count">32</biblScope><biblScope unit="part-chapter-count">16</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">David</forename><surname>Hutchison</surname></persName><affiliation><orgName type="institution">Lancaster University</orgName><address><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Takeo</forename><surname>Kanade</surname></persName><affiliation><orgName type="institution">Carnegie Mellon University</orgName><address><settlement>Pittsburgh</settlement><region>PA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Josef</forename><surname>Kittler</surname></persName><affiliation><orgName type="institution">University of Surrey</orgName><address><settlement>Guildford</settlement><country key="GB">UNITED KINGDOM</country></address></affiliation></editor><editor><persName><forename type="first">Jon</forename><forename type="first">M.</forename><surname>Kleinberg</surname></persName><affiliation><orgName type="institution">Cornell University</orgName><address><settlement>Ithaca</settlement><region>NY</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Friedemann</forename><surname>Mattern</surname></persName><affiliation><orgName type="institution">ETH Zurich</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">John</forename><forename type="first">C.</forename><surname>Mitchell</surname></persName><affiliation><orgName type="institution">Stanford University</orgName><address><settlement>CA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moni</forename><surname>Naor</surname></persName><affiliation><orgName type="institution">Weizmann Institute of Science</orgName><address><settlement>Rehovot</settlement><country key="IL">ISRAEL</country></address></affiliation></editor><editor><persName><forename type="first">Oscar</forename><surname>Nierstrasz</surname></persName><affiliation><orgName type="institution">University of Bern</orgName><address><country key="CH">SWITZERLAND</country></address></affiliation></editor><editor><persName><forename type="first">C.</forename><surname>Pandu Rangan</surname></persName><affiliation><orgName type="institution">Indian Institute of Technology</orgName><address><settlement>Madras</settlement><country key="IN">INDIA</country></address></affiliation></editor><editor><persName><forename type="first">Bernhard</forename><surname>Steffen</surname></persName><affiliation><orgName type="institution">University of Dortmund</orgName><address><country key="DE">GERMANY</country></address></affiliation></editor><editor><persName><forename type="first">Madhu</forename><surname>Sudan</surname></persName><affiliation><orgName type="institution">Massachusetts Institute of Technology</orgName><address><settlement>MA</settlement><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Demetri</forename><surname>Terzopoulos</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Los Angeles</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Dough</forename><surname>Tygar</surname></persName><affiliation><orgName type="institution">University of California</orgName><address><settlement>Berkeley</settlement><region>CA</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Moshe</forename><forename type="first">Y.</forename><surname>Vardi</surname></persName><affiliation><orgName type="institution">Rice University</orgName><address><settlement>Houston</settlement><region>TX</region><country key="US">UNITED STATES</country></address></affiliation></editor><editor><persName><forename type="first">Gerhard</forename><surname>Weikum</surname></persName><affiliation><orgName type="institution">Max-Planck Institute of Computer Science</orgName><address><settlement>Saarbruecken</settlement><country key="DE">GERMANY</country></address></affiliation></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.</p></abstract><textClass ana="keyword"><keywords xml:lang="en"><term>event B</term><term>pattern</term><term>distributed systems</term><term>refinement</term></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I14029</label><item><term type="Secondary" subtype="priority-1">Software Engineering</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-2">Logics and Meanings of Programs</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks 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 Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>David</GivenName><FamilyName>Hutchison</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Takeo</GivenName><FamilyName>Kanade</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Josef</GivenName><FamilyName>Kittler</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jon</GivenName><GivenName>M.</GivenName><FamilyName>Kleinberg</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff5"><EditorName DisplayOrder="Western"><GivenName>Friedemann</GivenName><FamilyName>Mattern</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff6"><EditorName DisplayOrder="Western"><GivenName>John</GivenName><GivenName>C.</GivenName><FamilyName>Mitchell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff7"><EditorName DisplayOrder="Western"><GivenName>Moni</GivenName><FamilyName>Naor</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff8"><EditorName DisplayOrder="Western"><GivenName>Oscar</GivenName><FamilyName>Nierstrasz</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff9"><EditorName DisplayOrder="Western"><GivenName>C.</GivenName><FamilyName>Pandu Rangan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff10"><EditorName DisplayOrder="Western"><GivenName>Bernhard</GivenName><FamilyName>Steffen</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff11"><EditorName DisplayOrder="Western"><GivenName>Madhu</GivenName><FamilyName>Sudan</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff12"><EditorName DisplayOrder="Western"><GivenName>Demetri</GivenName><FamilyName>Terzopoulos</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff13"><EditorName DisplayOrder="Western"><GivenName>Dough</GivenName><FamilyName>Tygar</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff14"><EditorName DisplayOrder="Western"><GivenName>Moshe</GivenName><GivenName>Y.</GivenName><FamilyName>Vardi</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff15"><EditorName DisplayOrder="Western"><GivenName>Gerhard</GivenName><FamilyName>Weikum</FamilyName></EditorName></Editor><Affiliation ID="Aff1"><OrgName>Lancaster University</OrgName><OrgAddress><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff3"><OrgName>University of Surrey</OrgName><OrgAddress><City>Guildford</City><Country>UK</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Cornell University</OrgName><OrgAddress><City>Ithaca</City><State>NY</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff5"><OrgName>ETH Zurich</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff6"><OrgName>Stanford University</OrgName><OrgAddress><City>CA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff7"><OrgName>Weizmann Institute of Science</OrgName><OrgAddress><City>Rehovot</City><Country>Israel</Country></OrgAddress></Affiliation><Affiliation ID="Aff8"><OrgName>University of Bern</OrgName><OrgAddress><Country>Switzerland</Country></OrgAddress></Affiliation><Affiliation ID="Aff9"><OrgName>Indian Institute of Technology</OrgName><OrgAddress><City>Madras</City><Country>India</Country></OrgAddress></Affiliation><Affiliation ID="Aff10"><OrgName>University of Dortmund</OrgName><OrgAddress><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff11"><OrgName>Massachusetts Institute of Technology</OrgName><OrgAddress><City>MA</City><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff12"><OrgName>University of California</OrgName><OrgAddress><City>Los Angeles</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff13"><OrgName>University of California</OrgName><OrgAddress><City>Berkeley</City><State>CA</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff14"><OrgName>Rice University</OrgName><OrgAddress><City>Houston</City><State>TX</State><Country>USA</Country></OrgAddress></Affiliation><Affiliation ID="Aff15"><OrgName>Max-Planck Institute of Computer Science</OrgName><OrgAddress><City>Saarbruecken</City><Country>Germany</Country></OrgAddress></Affiliation></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingDepth="2" NumberingStyle="ContentOnly" OutputMedium="All" TocLevels="0"><BookID>978-3-540-68761-0</BookID><BookTitle>B 2007: Formal Specification and Development in B</BookTitle><BookSubTitle>7th International Conference of B Users, Besançon, France, January 17-19, 2007. Proceedings</BookSubTitle><BookVolumeNumber>4355</BookVolumeNumber><BookSequenceNumber>4355</BookSequenceNumber><BookDOI>10.1007/11955757</BookDOI><BookTitleID>143304</BookTitleID><BookPrintISBN>978-3-540-68760-3</BookPrintISBN><BookElectronicISBN>978-3-540-68761-0</BookElectronicISBN><BookChapterCount>32</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2006</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I14029" Priority="1" Type="Secondary">Software Engineering</BookSubject><BookSubject Code="I1603X" Priority="2" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff16"><EditorName DisplayOrder="Western"><GivenName>Jacques</GivenName><FamilyName>Julliand</FamilyName></EditorName><Contact><Email>julliand@lifc.univ-fcomte.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff17"><EditorName DisplayOrder="Western"><GivenName>Olga</GivenName><FamilyName>Kouchnarenko</FamilyName></EditorName><Contact><Email>Olga.Kouchnarenko@lifc.univ-fcomte.fr</Email></Contact></Editor><Affiliation ID="Aff16"><OrgDivision>LIFC</OrgDivision><OrgName>Université de Franche-Comté</OrgName><OrgAddress><Street>16, route de Gray</Street><Postcode>F-25030</Postcode><City>Besançon Cedex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff17"><OrgName>LIFC – TFC Team</OrgName><OrgAddress><Street>16 route de Gray</Street><Postcode>F-25030</Postcode><City>Besançon</City></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Regular Papers</PartTitle><PartChapterCount>16</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>B 2007: Formal Specification and Development in B</BookTitle></PartContext></PartInfo><Chapter ID="Chap13" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingDepth="2" NumberingStyle="ContentOnly" TocLevels="0"><ChapterID>13</ChapterID><ChapterDOI>10.1007/11955757_13</ChapterDOI><ChapterSequenceNumber>13</ChapterSequenceNumber><ChapterTitle Language="En">Time Constraint Patterns for Event B Development</ChapterTitle><ChapterFirstPage>140</ChapterFirstPage><ChapterLastPage>154</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2006</CopyrightYear></ChapterCopyright><ChapterGrants 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></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>2</PartID><BookID>978-3-540-68761-0</BookID><BookTitle>B 2007: Formal Specification and Development in B</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff18 Aff20"><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Cansell</FamilyName></AuthorName><Contact><Email>cansell@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff19 Aff20"><AuthorName DisplayOrder="Western"><GivenName>Dominique</GivenName><FamilyName>Méry</FamilyName></AuthorName><Contact><Email>mery@loria.fr</Email></Contact></Author><Author AffiliationIDS="Aff19 Aff20"><AuthorName DisplayOrder="Western"><GivenName>Joris</GivenName><FamilyName>Rehm</FamilyName></AuthorName><Contact><Email>rehm@loria.fr</Email></Contact></Author><Affiliation ID="Aff18"><OrgName>Université de Metz</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff19"><OrgName>Université Henri Poincaré Nancy 1</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation><Affiliation ID="Aff20"><OrgName>LORIA</OrgName><OrgAddress><Postbox>BP 239</Postbox><Postcode>54506</Postcode><City>Vandœvre-lès-Nancy</City><Country>France</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.</Para></Abstract><KeywordGroup Language="En"><Heading>Keywords</Heading><Keyword>event B</Keyword><Keyword>pattern</Keyword><Keyword>distributed systems</Keyword><Keyword>refinement</Keyword></KeywordGroup></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Time Constraint Patterns for Event B Development</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Time Constraint Patterns for Event B Development</title></titleInfo><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Cansell</namePart><affiliation>Université de Metz, </affiliation><affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</affiliation><affiliation>E-mail: cansell@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Méry</namePart><affiliation>Université Henri Poincaré Nancy 1, </affiliation><affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</affiliation><affiliation>E-mail: mery@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Joris</namePart><namePart type="family">Rehm</namePart><affiliation>Université Henri Poincaré Nancy 1, </affiliation><affiliation>LORIA, BP 239, 54506, Vandœvre-lès-Nancy, France</affiliation><affiliation>E-mail: rehm@loria.fr</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2006</dateIssued><copyrightDate encoding="w3cdtf">2006</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract lang="en">Abstract: Distributed applications are based on algorithms which should be able to deal with time constraints. It is mandatory to express time constraints in (mathematical) models and the current work intends to integrate time constraints in the modelling process based on event B models and refinement. The starting point of our work is the event B development of the IEEE 1394 leader election protocol; from standard documents, we derive temporal requirements to solve the contention problem and we propose a method for introducing time constraints using a pattern. The pattern captures time constraints in a generic event B development and it is applied to the IEEE 1394 case study.</abstract><subject lang="en"><genre>Keywords</genre><topic>event B</topic><topic>pattern</topic><topic>distributed systems</topic><topic>refinement</topic></subject><relatedItem type="host"><titleInfo><title>B 2007: Formal Specification and Development in B</title><subTitle>7th International Conference of B Users, Besançon, France, January 17-19, 2007. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Jacques</namePart><namePart type="family">Julliand</namePart><affiliation>LIFC, Université de Franche-Comté, 16, route de Gray, F-25030, Besançon Cedex, France</affiliation><affiliation>E-mail: julliand@lifc.univ-fcomte.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Olga</namePart><namePart type="family">Kouchnarenko</namePart><affiliation>LIFC – TFC Team, 16 route de Gray, F-25030, Besançon</affiliation><affiliation>E-mail: Olga.Kouchnarenko@lifc.univ-fcomte.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2006</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I14029">Software Engineering</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/11955757</identifier><identifier type="ISBN">978-3-540-68760-3</identifier><identifier type="eISBN">978-3-540-68761-0</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">143304</identifier><identifier type="BookID">978-3-540-68761-0</identifier><identifier type="BookChapterCount">32</identifier><identifier type="BookVolumeNumber">4355</identifier><identifier type="BookSequenceNumber">4355</identifier><identifier type="PartChapterCount">16</identifier><part><date>2006</date><detail type="part"><title>Regular Papers</title></detail><detail type="volume"><number>4355</number><caption>vol.</caption></detail><extent unit="pages"><start>140</start><end>154</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">David</namePart><namePart type="family">Hutchison</namePart><affiliation>Lancaster University, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Takeo</namePart><namePart type="family">Kanade</namePart><affiliation>Carnegie Mellon University, Pittsburgh, PA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Josef</namePart><namePart type="family">Kittler</namePart><affiliation>University of Surrey, Guildford, UK</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jon</namePart><namePart type="given">M.</namePart><namePart type="family">Kleinberg</namePart><affiliation>Cornell University, Ithaca, NY, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Friedemann</namePart><namePart type="family">Mattern</namePart><affiliation>ETH Zurich, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">John</namePart><namePart type="given">C.</namePart><namePart type="family">Mitchell</namePart><affiliation>Stanford University, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moni</namePart><namePart type="family">Naor</namePart><affiliation>Weizmann Institute of Science, Rehovot, Israel</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Oscar</namePart><namePart type="family">Nierstrasz</namePart><affiliation>University of Bern, Switzerland</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">C.</namePart><namePart type="family">Pandu Rangan</namePart><affiliation>Indian Institute of Technology, Madras, India</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Bernhard</namePart><namePart type="family">Steffen</namePart><affiliation>University of Dortmund, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Madhu</namePart><namePart type="family">Sudan</namePart><affiliation>Massachusetts Institute of Technology, MA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Demetri</namePart><namePart type="family">Terzopoulos</namePart><affiliation>University of California, Los Angeles, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Dough</namePart><namePart type="family">Tygar</namePart><affiliation>University of California, Berkeley, CA, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Moshe</namePart><namePart type="given">Y.</namePart><namePart type="family">Vardi</namePart><affiliation>Rice University, Houston, TX, USA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Gerhard</namePart><namePart type="family">Weikum</namePart><affiliation>Max-Planck Institute of Computer Science, Saarbruecken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">2006</copyrightDate><issuance>serial</issuance></originInfo><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</recordOrigin></recordInfo></relatedItem><identifier type="istex">CAF1976E06FD7349E71DF25222E083D51C33A992</identifier><identifier type="ark">ark:/67375/HCB-03FPWSX2-3</identifier><identifier type="DOI">10.1007/11955757_13</identifier><identifier type="ChapterID">13</identifier><identifier type="ChapterID">Chap13</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2006</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2006</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-03FPWSX2-3/record.json</uri></json:item></metadata></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 003015 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003015 | 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:CAF1976E06FD7349E71DF25222E083D51C33A992
|texte= Time Constraint Patterns for Event B Development
}}
| This area was generated with Dilib version V0.6.33. |  |