On using temporal logic for refinement and compositional verification of concurrent systems
Identifieur interne : 000560 ( Istex/Corpus ); précédent : 000559; suivant : 000561On using temporal logic for refinement and compositional verification of concurrent systems
Auteurs : Abdelillah Mokkedem ; Dominique MérySource :
- Theoretical Computer Science [ 0304-3975 ] ; 1995.
English descriptors
- Teeft :
- Abstract semantics, Abstraction problem, Axiom, Behaviour, Compatible modules, Composition principles, Compositional, Compositional rule, Compositional verification, Computer science, Concurrent, Concurrent program, Concurrent programs, Concurrent systems, Consum, Control variables, Different states, Environment modes, Environment transitions, Eventuality, Eventuality properties, Execution sequence, Execution sequences, Fair transition system, Fairness requirements, Flexible variables, Individual transitions, Init, Integer, Interface, Internal transitions, Invariance, Lamport, Lecture notes, Liveness properties, Local variables, Manna, Module, Mokkedem, Next operator, Next state, Observable variables, Open semantics, Parallel composition, Parallel programs, Pnueli, Predicate, Program equivalence, Programming notation, Proof system, Quantifier, Resp, Rigid variables, Semantic description, Semantics, Sentence symbol, Soundness, Specification, Specification module, Springer, State formula, State formulas, Stuttering, Stuttering steps, Temporal, Temporal formulas, Temporal logic, Temporal proof system, Temporal replacement, Temporal semantics, Temporal validity, Theoretical computer science, Transition relation.
Abstract
Abstract: A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under w-stuttering and, thus, provides a fully abstract semantics with respect to some chosen observation level w. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program design and implementation of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.
Url:
DOI: 10.1016/0304-3975(94)00206-X
Links to Exploration step
ISTEX:1931E8D96B14F8280C90FFB68EDC0ACE43710CD6Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title>On using temporal logic for refinement and compositional verification of concurrent systems</title><author><name sortKey="Mokkedem, Abdelillah" sort="Mokkedem, Abdelillah" uniqKey="Mokkedem A" first="Abdelillah" last="Mokkedem">Abdelillah Mokkedem</name><affiliation><mods:affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</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>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:1931E8D96B14F8280C90FFB68EDC0ACE43710CD6</idno><date when="1995" year="1995">1995</date><idno type="doi">10.1016/0304-3975(94)00206-X</idno><idno type="url">https://api.istex.fr/ark:/67375/6H6-QX2ZL52X-C/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000560</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000560</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a">On using temporal logic for refinement and compositional verification of concurrent systems</title><author><name sortKey="Mokkedem, Abdelillah" sort="Mokkedem, Abdelillah" uniqKey="Mokkedem A" first="Abdelillah" last="Mokkedem">Abdelillah Mokkedem</name><affiliation><mods:affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</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>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="ISSN">0304-3975</idno><imprint><publisher>ELSEVIER</publisher><date type="published" when="1995">1995</date><biblScope unit="volume">140</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="95">95</biblScope><biblScope unit="page" to="138">138</biblScope></imprint><idno type="ISSN">0304-3975</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0304-3975</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="Teeft" xml:lang="en"><term>Abstract semantics</term><term>Abstraction problem</term><term>Axiom</term><term>Behaviour</term><term>Compatible modules</term><term>Composition principles</term><term>Compositional</term><term>Compositional rule</term><term>Compositional verification</term><term>Computer science</term><term>Concurrent</term><term>Concurrent program</term><term>Concurrent programs</term><term>Concurrent systems</term><term>Consum</term><term>Control variables</term><term>Different states</term><term>Environment modes</term><term>Environment transitions</term><term>Eventuality</term><term>Eventuality properties</term><term>Execution sequence</term><term>Execution sequences</term><term>Fair transition system</term><term>Fairness requirements</term><term>Flexible variables</term><term>Individual transitions</term><term>Init</term><term>Integer</term><term>Interface</term><term>Internal transitions</term><term>Invariance</term><term>Lamport</term><term>Lecture notes</term><term>Liveness properties</term><term>Local variables</term><term>Manna</term><term>Module</term><term>Mokkedem</term><term>Next operator</term><term>Next state</term><term>Observable variables</term><term>Open semantics</term><term>Parallel composition</term><term>Parallel programs</term><term>Pnueli</term><term>Predicate</term><term>Program equivalence</term><term>Programming notation</term><term>Proof system</term><term>Quantifier</term><term>Resp</term><term>Rigid variables</term><term>Semantic description</term><term>Semantics</term><term>Sentence symbol</term><term>Soundness</term><term>Specification</term><term>Specification module</term><term>Springer</term><term>State formula</term><term>State formulas</term><term>Stuttering</term><term>Stuttering steps</term><term>Temporal</term><term>Temporal formulas</term><term>Temporal logic</term><term>Temporal proof system</term><term>Temporal replacement</term><term>Temporal semantics</term><term>Temporal validity</term><term>Theoretical computer science</term><term>Transition relation</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under w-stuttering and, thus, provides a fully abstract semantics with respect to some chosen observation level w. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program design and implementation of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.</div></front></TEI><istex><corpusName>elsevier</corpusName><keywords><teeft><json:string>module</json:string><json:string>semantics</json:string><json:string>mokkedem</json:string><json:string>theoretical computer science</json:string><json:string>stuttering</json:string><json:string>temporal logic</json:string><json:string>axiom</json:string><json:string>consum</json:string><json:string>concurrent programs</json:string><json:string>concurrent systems</json:string><json:string>quantifier</json:string><json:string>init</json:string><json:string>resp</json:string><json:string>compositional</json:string><json:string>environment transitions</json:string><json:string>computer science</json:string><json:string>pnueli</json:string><json:string>invariance</json:string><json:string>proof system</json:string><json:string>springer</json:string><json:string>manna</json:string><json:string>lamport</json:string><json:string>flexible variables</json:string><json:string>rigid variables</json:string><json:string>specification</json:string><json:string>predicate</json:string><json:string>state formula</json:string><json:string>temporal semantics</json:string><json:string>compositional verification</json:string><json:string>interface</json:string><json:string>behaviour</json:string><json:string>temporal</json:string><json:string>soundness</json:string><json:string>lecture notes</json:string><json:string>temporal validity</json:string><json:string>temporal proof system</json:string><json:string>state formulas</json:string><json:string>specification module</json:string><json:string>stuttering steps</json:string><json:string>internal transitions</json:string><json:string>individual transitions</json:string><json:string>next operator</json:string><json:string>temporal replacement</json:string><json:string>parallel composition</json:string><json:string>environment modes</json:string><json:string>concurrent</json:string><json:string>eventuality</json:string><json:string>parallel programs</json:string><json:string>open semantics</json:string><json:string>observable variables</json:string><json:string>semantic description</json:string><json:string>execution sequences</json:string><json:string>transition relation</json:string><json:string>concurrent program</json:string><json:string>compositional rule</json:string><json:string>execution sequence</json:string><json:string>compatible modules</json:string><json:string>local variables</json:string><json:string>abstract semantics</json:string><json:string>different states</json:string><json:string>program equivalence</json:string><json:string>abstraction problem</json:string><json:string>next state</json:string><json:string>temporal formulas</json:string><json:string>programming notation</json:string><json:string>control variables</json:string><json:string>liveness properties</json:string><json:string>sentence symbol</json:string><json:string>fairness requirements</json:string><json:string>eventuality properties</json:string><json:string>composition principles</json:string><json:string>fair transition system</json:string><json:string>integer</json:string><json:string>verification</json:string><json:string>notation</json:string><json:string>logic</json:string></teeft></keywords><author><json:item><name>Abdelillah Mokkedem</name><affiliations><json:string>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</json:string></affiliations></json:item><json:item><name>Dominique Méry</name><affiliations><json:string>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</json:string></affiliations></json:item></author><arkIstex>ark:/67375/6H6-QX2ZL52X-C</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>Full-length article</json:string></originalGenre><abstract>Abstract: A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under w-stuttering and, thus, provides a fully abstract semantics with respect to some chosen observation level w. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program design and implementation of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.</abstract><qualityIndicators><score>8.02</score><pdfWordCount>12907</pdfWordCount><pdfCharCount>77436</pdfCharCount><pdfVersion>1.2</pdfVersion><pdfPageCount>44</pdfPageCount><pdfPageSize>468 x 684 pts</pdfPageSize><refBibsNative>true</refBibsNative><abstractWordCount>85</abstractWordCount><abstractCharCount>609</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>On using temporal logic for refinement and compositional verification of concurrent systems</title><pii><json:string>0304-3975(94)00206-X</json:string></pii><genre><json:string>research-article</json:string></genre><serie><title>Tech. Report 86</title><language><json:string>unknown</json:string></language></serie><host><title>Theoretical Computer Science</title><language><json:string>unknown</json:string></language><publicationDate>1995</publicationDate><issn><json:string>0304-3975</json:string></issn><pii><json:string>S0304-3975(00)X0036-9</json:string></pii><volume>140</volume><issue>1</issue><pages><first>95</first><last>138</last></pages><genre><json:string>journal</json:string></genre><conference><json:item><name>Third International Conference on Algebraic Methodology of Software Technology, University of Twente, Enschede, The Netherlands AMAST '93 19930621 19930625</name></json:item></conference><editor><json:item><name>G. Scollo</name></json:item><json:item><name>T. Rus</name></json:item></editor></host><namedEntities><unitex><date><json:string>19930621</json:string><json:string>1995</json:string></date><geogName></geogName><orgName></orgName><orgName_funder></orgName_funder><orgName_provider></orgName_provider><persName><json:string>D. Mhry</json:string><json:string>F. Syntax</json:string><json:string>D. Mkry</json:string><json:string>F. Case</json:string><json:string>F. Proof</json:string><json:string>A. Mokkedem</json:string><json:string>T. Rus</json:string><json:string>BI InI</json:string><json:string>F. Note</json:string><json:string>F. Proposition</json:string></persName><placeName><json:string>Sy</json:string></placeName><ref_url></ref_url><ref_bibl><json:string>[4]</json:string><json:string>[12]</json:string><json:string>[6]</json:string><json:string>[22]</json:string><json:string>[17]</json:string><json:string>[21]</json:string><json:string>[8,9]</json:string><json:string>[13,17]</json:string><json:string>[20]</json:string><json:string>[26]</json:string><json:string>[24]</json:string><json:string>[14,16]</json:string></ref_bibl><bibl></bibl></unitex></namedEntities><ark><json:string>ark:/67375/6H6-QX2ZL52X-C</json:string></ark><categories><wos><json:string>1 - science</json:string><json:string>2 - computer science, theory & methods</json:string></wos><scienceMetrix><json:string>1 - applied sciences</json:string><json:string>2 - information & communication technologies</json:string><json:string>3 - computation theory & mathematics</json:string></scienceMetrix><scopus><json:string>1 - Physical Sciences</json:string><json:string>2 - Computer Science</json:string><json:string>3 - General Computer Science</json:string><json:string>1 - Physical Sciences</json:string><json:string>2 - Mathematics</json:string><json:string>3 - Theoretical Computer Science</json:string></scopus><inist><json:string>1 - sciences appliquees, technologies et medecines</json:string><json:string>2 - sciences exactes et technologie</json:string><json:string>3 - terre, ocean, espace</json:string><json:string>4 - sciences de la terre</json:string></inist></categories><publicationDate>1995</publicationDate><copyrightDate>1995</copyrightDate><doi><json:string>10.1016/0304-3975(94)00206-X</json:string></doi><id>1931E8D96B14F8280C90FFB68EDC0ACE43710CD6</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-QX2ZL52X-C/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-QX2ZL52X-C/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/6H6-QX2ZL52X-C/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a">On using temporal logic for refinement and compositional verification of concurrent systems</title></titleStmt><publicationStmt><authority>ISTEX</authority><publisher scheme="https://scientific-publisher.data.istex.fr">ELSEVIER</publisher><availability><licence><p>elsevier</p></licence></availability><p scheme="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M"></p><date>1995</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></notesStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a">On using temporal logic for refinement and compositional verification of concurrent systems</title><author xml:id="author-0000"><persName><forename type="first">Abdelillah</forename><surname>Mokkedem</surname></persName><note type="correspondence"><p>Corresponding author.</p></note><affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</affiliation></author><author xml:id="author-0001"><persName><forename type="first">Dominique</forename><surname>Méry</surname></persName><affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</affiliation></author><idno type="istex">1931E8D96B14F8280C90FFB68EDC0ACE43710CD6</idno><idno type="ark">ark:/67375/6H6-QX2ZL52X-C</idno><idno type="DOI">10.1016/0304-3975(94)00206-X</idno><idno type="PII">0304-3975(94)00206-X</idno></analytic><monogr><title level="j">Theoretical Computer Science</title><title level="j" type="abbrev">TCS</title><idno type="pISSN">0304-3975</idno><idno type="PII">S0304-3975(00)X0036-9</idno><meeting><addName>Third International Conference on Algebraic Methodology of Software Technology, University of Twente, Enschede, The Netherlands</addName><addName>AMAST '93</addName><date>19930621</date><date>19930625</date></meeting><editor xml:id="book-author-0000"><persName>G. Scollo</persName></editor><editor xml:id="book-author-0001"><persName>T. Rus</persName></editor><imprint><publisher>ELSEVIER</publisher><date type="published" when="1995"></date><biblScope unit="volume">140</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="95">95</biblScope><biblScope unit="page" to="138">138</biblScope></imprint></monogr></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>1995</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under w-stuttering and, thus, provides a fully abstract semantics with respect to some chosen observation level w. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program design and implementation of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.</p></abstract></profileDesc><revisionDesc><change when="1995">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/6H6-QX2ZL52X-C/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Elsevier, elements deleted: tail"><istex:xmlDeclaration>version="1.0" encoding="utf-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//ES//DTD journal article DTD version 4.5.2//EN//XML" URI="art452.dtd" name="istex:docType"></istex:docType><istex:document><converted-article version="4.5.2" docsubtype="fla"><item-info><jid>TCS</jid><aid>9400206X</aid><ce:pii>0304-3975(94)00206-X</ce:pii><ce:doi>10.1016/0304-3975(94)00206-X</ce:doi><ce:copyright type="unknown" year="1995"></ce:copyright></item-info><head><ce:title>On using temporal logic for refinement and compositional verification of concurrent systems</ce:title><ce:author-group><ce:author><ce:given-name>Abdelillah</ce:given-name><ce:surname>Mokkedem</ce:surname><ce:cross-ref refid="COR1"><ce:sup>∗</ce:sup></ce:cross-ref></ce:author><ce:author><ce:given-name>Dominique</ce:given-name><ce:surname>Méry</ce:surname></ce:author><ce:affiliation><ce:textfn>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</ce:textfn></ce:affiliation><ce:correspondence id="COR1"><ce:label>∗</ce:label><ce:text>Corresponding author.</ce:text></ce:correspondence></ce:author-group><ce:abstract><ce:section-title>Abstract</ce:section-title><ce:abstract-sec><ce:simple-para>A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under <ce:italic>w-stuttering</ce:italic> and, thus, provides a fully abstract semantics with respect to some chosen observation level <ce:italic>w</ce:italic>. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program <ce:italic>design</ce:italic> and <ce:italic>implementation</ce:italic> of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.</ce:simple-para></ce:abstract-sec></ce:abstract></head></converted-article></istex:document></istex:metadataXml><mods version="3.6"><titleInfo><title>On using temporal logic for refinement and compositional verification of concurrent systems</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>On using temporal logic for refinement and compositional verification of concurrent systems</title></titleInfo><name type="personal"><namePart type="given">Abdelillah</namePart><namePart type="family">Mokkedem</namePart><affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</affiliation><description>Corresponding author.</description><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Dominique</namePart><namePart type="family">Méry</namePart><affiliation>CRIN-CNRS & INRIA-Lorraine, BP239, 54506 Vandœuvre-lès-Nancy, Cedex, France</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="research-article" displayLabel="Full-length article" 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>ELSEVIER</publisher><dateIssued encoding="w3cdtf">1995</dateIssued><copyrightDate encoding="w3cdtf">1995</copyrightDate></originInfo><language><languageTerm type="code" authority="iso639-2b">eng</languageTerm><languageTerm type="code" authority="rfc3066">en</languageTerm></language><abstract lang="en">Abstract: A simple and elegant formulation of compositional proof systems for concurrent programs results from a refinement of temporal logic semantics. The refined temporal language we propose is closed under w-stuttering and, thus, provides a fully abstract semantics with respect to some chosen observation level w. This avoids incorporating irrelevant detail in the temporal semantics of parallel programs. Besides compositional verification, concurrent program design and implementation of a coarser-grained program by a finer-grained one, are easily practicable in the setting of the new temporal logic.</abstract><relatedItem type="host"><titleInfo><title>Theoretical Computer Science</title></titleInfo><titleInfo type="abbreviated"><title>TCS</title></titleInfo><name type="conference"><namePart>Third International Conference on Algebraic Methodology of Software Technology, University of Twente, Enschede, The Netherlands</namePart><namePart>AMAST '93</namePart><namePart type="date">19930621</namePart><namePart type="date">19930625</namePart></name><name type="personal"><namePart>G. Scollo</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart>T. Rus</namePart><role><roleTerm type="text">editor</roleTerm></role></name><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>ELSEVIER</publisher><dateIssued encoding="w3cdtf">1995</dateIssued></originInfo><identifier type="ISSN">0304-3975</identifier><identifier type="PII">S0304-3975(00)X0036-9</identifier><part><date>1995</date><detail type="issue"><title>Third International Conference on Algebraic Methodology of Software Technology, University of Twente, Enschede, The Netherlands</title></detail><detail type="volume"><number>140</number><caption>vol.</caption></detail><detail type="issue"><number>1</number><caption>no.</caption></detail><extent unit="issue-pages"><start>1</start><end>199</end></extent><extent unit="pages"><start>95</start><end>138</end></extent></part></relatedItem><identifier type="istex">1931E8D96B14F8280C90FFB68EDC0ACE43710CD6</identifier><identifier type="ark">ark:/67375/6H6-QX2ZL52X-C</identifier><identifier type="DOI">10.1016/0304-3975(94)00206-X</identifier><identifier type="PII">0304-3975(94)00206-X</identifier><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-HKKZVM7B-M">elsevier</recordContentSource></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/6H6-QX2ZL52X-C/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 000560 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000560 | 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:1931E8D96B14F8280C90FFB68EDC0ACE43710CD6
|texte= On using temporal logic for refinement and compositional verification of concurrent systems
}}
| This area was generated with Dilib version V0.6.33. |  |