InforLorV4, PascalFrancis, Corpus, bibRecord, 000D63

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

Identifieur interne : 000D63 ( PascalFrancis/Corpus ); précédent : 000D62; suivant : 000D64

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

Auteurs : ABDELILLAH MOKKEDEM ; 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

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

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`

Format Inist (serveur)

NO :	PASCAL 95-0222589 INIST
ET :	On using temporal logic for refinement and compositional verification of concurrent systems
AU :	ABDELILLAH MOKKEDEM; MERY (D.); SCOLLO (G.); RUS (T.)
AF :	CNRS-CRIN/54506 Vandœuvre-lès-Nancy/France; INRIA-Lorraine/54506 Vandœuvre-lès-Nancy/France; Univ. Twente, dep. computer sci./7500 AE Enschede/Pays-Bas (1 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 1995; Vol. 140; No. 1; Pp. 95-138; Bibl. 27 ref.
LA :	Anglais
EA :	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
CC :	001D02A07
FD :	Programme concurrent; Logique temporelle; Sémantique formelle; Abstraction; Affinement; Vérification; Programme IPL; Logique MTL; Système preuve; Principe composition
ED :	Concurrent program; Temporal logic; Formal semantics; Abstraction; Refinement; Verification
GD :	Eichen
SD :	Programa competidor; Lógica temporal; Semántica formal; Abstracción; Afinamiento; Verificación
LO :	INIST-17243.354000059901310040
ID :	95-0222589

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><inist:fA14 i1="01"><s1>CNRS-CRIN</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>INRIA-Lorraine</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
</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>
</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><inist:fA14 i1="01"><s1>CNRS-CRIN</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
</affiliation>
<affiliation><inist:fA14 i1="02"><s1>INRIA-Lorraine</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
</inist:fA14>
</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>
<server><NO>PASCAL 95-0222589 INIST</NO>
<ET>On using temporal logic for refinement and compositional verification of concurrent systems</ET>
<AU>ABDELILLAH MOKKEDEM; MERY (D.); SCOLLO (G.); RUS (T.)</AU>
<AF>CNRS-CRIN/54506 Vandœuvre-lès-Nancy/France; INRIA-Lorraine/54506 Vandœuvre-lès-Nancy/France; Univ. Twente, dep. computer sci./7500 AE Enschede/Pays-Bas (1 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Theoretical computer science; ISSN 0304-3975; Coden TCSCDI; Pays-Bas; Da. 1995; Vol. 140; No. 1; Pp. 95-138; Bibl. 27 ref.</SO>
<LA>Anglais</LA>
<EA>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</EA>
<CC>001D02A07</CC>
<FD>Programme concurrent; Logique temporelle; Sémantique formelle; Abstraction; Affinement; Vérification; Programme IPL; Logique MTL; Système preuve; Principe composition</FD>
<ED>Concurrent program; Temporal logic; Formal semantics; Abstraction; Refinement; Verification</ED>
<GD>Eichen</GD>
<SD>Programa competidor; Lógica temporal; Semántica formal; Abstracción; Afinamiento; Verificación</SD>
<LO>INIST-17243.354000059901310040</LO>
<ID>95-0222589</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

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

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

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

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |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

Notice en format standard (ISO 2709)

Format Inist (serveur)

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