InforLorV4, PascalFrancis, Curation, bibRecord, 000B31

On using temporal logic for refinement and compositional verification of concurrent systems

Identifieur interne : 000B31 ( PascalFrancis/Curation ); précédent : 000B30; suivant : 000B32

On using temporal logic for refinement and compositional verification of concurrent systems

Auteurs : ABDELILLAH MOKKEDEM [France] ; D. Mery

Source :

Theoretical computer science [ 0304-3975 ] ; 1995.

RBID : Pascal:95-0222589

Descripteurs français

Pascal (Inist)
- Programme concurrent, Logique temporelle, Sémantique formelle, Abstraction, Affinement, Vérification, Programme IPL, Logique MTL, Système preuve, Principe composition.

English descriptors

KwdEn :
- Abstraction, Concurrent program, Formal semantics, Refinement, Temporal logic, Verification.

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

A01	`01`	`1`		`@0 0304-3975`
A02	`01`			`@0 TCSCDI`
A03		`1`		`@0 Theor. comput. sci.`
A05				`@2 140`
A06				`@2 1`
A08	`01`	`1`	`ENG`	`@1 On using temporal logic for refinement and compositional verification of concurrent systems`
A11	`01`	`1`		`@1 ABDELILLAH MOKKEDEM`
A11	`02`	`1`		`@1 MERY (D.)`
A12	`01`	`1`		`@1 SCOLLO (G.) @9 ed.`
A12	`02`	`1`		`@1 RUS (T.) @9 ed.`
A14	`01`			`@1 CNRS-CRIN @2 54506 Vandœuvre-lès-Nancy @3 FRA`
A14	`02`			`@1 INRIA-Lorraine @2 54506 Vandœuvre-lès-Nancy @3 FRA`
A15	`01`			`@1 Univ. Twente, dep. computer sci. @2 7500 AE Enschede @3 NLD @Z 1 aut.`
A20				`@1 95-138`
A21				`@1 1995`
A23	`01`			`@0 ENG`
A43	`01`			`@1 INIST @2 17243 @5 354000059901310040`
A44				`@0 0000`
A45				`@0 27 ref.`
A47	`01`	`1`		`@0 95-0222589`
A60				`@1 P @2 C`
A61				`@0 A`
A64	`01`	`1`		`@0 Theoretical computer science`
A66	`01`			`@0 NLD`
C01	`01`		`ENG`	@0 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
C02	`01`	`X`		`@0 001D02A07`
C03	`01`	`X`	`FRE`	`@0 Programme concurrent @5 01`
C03	`01`	`X`	`ENG`	`@0 Concurrent program @5 01`
C03	`01`	`X`	`SPA`	`@0 Programa competidor @5 01`
C03	`02`	`X`	`FRE`	`@0 Logique temporelle @5 02`
C03	`02`	`X`	`ENG`	`@0 Temporal logic @5 02`
C03	`02`	`X`	`SPA`	`@0 Lógica temporal @5 02`
C03	`03`	`X`	`FRE`	`@0 Sémantique formelle @5 04`
C03	`03`	`X`	`ENG`	`@0 Formal semantics @5 04`
C03	`03`	`X`	`SPA`	`@0 Semántica formal @5 04`
C03	`04`	`X`	`FRE`	`@0 Abstraction @5 05`
C03	`04`	`X`	`ENG`	`@0 Abstraction @5 05`
C03	`04`	`X`	`SPA`	`@0 Abstracción @5 05`
C03	`05`	`X`	`FRE`	`@0 Affinement @5 06`
C03	`05`	`X`	`ENG`	`@0 Refinement @5 06`
C03	`05`	`X`	`SPA`	`@0 Afinamiento @5 06`
C03	`06`	`X`	`FRE`	`@0 Vérification @5 07`
C03	`06`	`X`	`ENG`	`@0 Verification @5 07`
C03	`06`	`X`	`GER`	`@0 Eichen @5 07`
C03	`06`	`X`	`SPA`	`@0 Verificación @5 07`
C03	`07`	`X`	`FRE`	`@0 Programme IPL @4 INC @5 92`
C03	`08`	`X`	`FRE`	`@0 Logique MTL @4 INC @5 93`
C03	`09`	`X`	`FRE`	`@0 Système preuve @4 INC @5 94`
C03	`10`	`X`	`FRE`	`@0 Principe composition @4 INC @5 95`
N21				`@1 130`

A30	`01`	`1`	`ENG`	`@1 AMAST '93 : international conference on algebraic methodology of software technology @2 3 @3 Enschede NLD @4 1993-06-21`

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

to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000D63

Links to Exploration step

Pascal:95-0222589

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">On using temporal logic for refinement and compositional verification of concurrent systems</title>
<author><name sortKey="Abdelillah Mokkedem" sort="Abdelillah Mokkedem" uniqKey="Abdelillah Mokkedem" last="Abdelillah Mokkedem">ABDELILLAH MOKKEDEM</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>CNRS-CRIN</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
<country>France</country>
</affiliation>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA-Lorraine</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">95-0222589</idno>
<date when="1995">1995</date>
<idno type="stanalyst">PASCAL 95-0222589 INIST</idno>
<idno type="RBID">Pascal:95-0222589</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000D63</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000B31</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">On using temporal logic for refinement and compositional verification of concurrent systems</title>
<author><name sortKey="Abdelillah Mokkedem" sort="Abdelillah Mokkedem" uniqKey="Abdelillah Mokkedem" last="Abdelillah Mokkedem">ABDELILLAH MOKKEDEM</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>CNRS-CRIN</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
<country>France</country>
</affiliation>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>INRIA-Lorraine</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
</author>
</analytic>
<series><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
<imprint><date when="1995">1995</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Theoretical computer science</title>
<title level="j" type="abbreviated">Theor. comput. sci.</title>
<idno type="ISSN">0304-3975</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Abstraction</term>
<term>Concurrent program</term>
<term>Formal semantics</term>
<term>Refinement</term>
<term>Temporal logic</term>
<term>Verification</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Programme concurrent</term>
<term>Logique temporelle</term>
<term>Sémantique formelle</term>
<term>Abstraction</term>
<term>Affinement</term>
<term>Vérification</term>
<term>Programme IPL</term>
<term>Logique MTL</term>
<term>Système preuve</term>
<term>Principe composition</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">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>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0304-3975</s0>
</fA01>
<fA02 i1="01"><s0>TCSCDI</s0>
</fA02>
<fA03 i2="1"><s0>Theor. comput. sci.</s0>
</fA03>
<fA05><s2>140</s2>
</fA05>
<fA06><s2>1</s2>
</fA06>
<fA08 i1="01" i2="1" l="ENG"><s1>On using temporal logic for refinement and compositional verification of concurrent systems</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>ABDELILLAH MOKKEDEM</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>MERY (D.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>SCOLLO (G.)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>RUS (T.)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>CNRS-CRIN</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</fA14>
<fA14 i1="02"><s1>INRIA-Lorraine</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</fA14>
<fA15 i1="01"><s1>Univ. Twente, dep. computer sci.</s1>
<s2>7500 AE Enschede</s2>
<s3>NLD</s3>
<sZ>1 aut.</sZ>
</fA15>
<fA20><s1>95-138</s1>
</fA20>
<fA21><s1>1995</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>17243</s2>
<s5>354000059901310040</s5>
</fA43>
<fA44><s0>0000</s0>
</fA44>
<fA45><s0>27 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>95-0222589</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Theoretical computer science</s0>
</fA64>
<fA66 i1="01"><s0>NLD</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>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</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02A07</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Programme concurrent</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Concurrent program</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Programa competidor</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Logique temporelle</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Temporal logic</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Lógica temporal</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Sémantique formelle</s0>
<s5>04</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Formal semantics</s0>
<s5>04</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Semántica formal</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Abstraction</s0>
<s5>05</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Abstraction</s0>
<s5>05</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Abstracción</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Affinement</s0>
<s5>06</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Refinement</s0>
<s5>06</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Afinamiento</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Vérification</s0>
<s5>07</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Verification</s0>
<s5>07</s5>
</fC03>
<fC03 i1="06" i2="X" l="GER"><s0>Eichen</s0>
<s5>07</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Verificación</s0>
<s5>07</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Programme IPL</s0>
<s4>INC</s4>
<s5>92</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Logique MTL</s0>
<s4>INC</s4>
<s5>93</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Système preuve</s0>
<s4>INC</s4>
<s5>94</s5>
</fC03>
<fC03 i1="10" i2="X" l="FRE"><s0>Principe composition</s0>
<s4>INC</s4>
<s5>95</s5>
</fC03>
<fN21><s1>130</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>AMAST '93 : international conference on algebraic methodology of software technology</s1>
<s2>3</s2>
<s3>Enschede NLD</s3>
<s4>1993-06-21</s4>
</fA30>
</pR>
</standard>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Curation

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000B31 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000B31 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Curation
   |type=    RBID
   |clé=     Pascal:95-0222589
   |texte=   On using temporal logic for refinement and compositional verification of concurrent systems
}}

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

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

Serveur d'exploration sur la recherche en informatique en Lorraine

On using temporal logic for refinement and compositional verification of concurrent systems

On using temporal logic for refinement and compositional verification of concurrent systems

Source :

Descripteurs français

English descriptors

Abstract

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

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

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