InforLorV4, PascalFrancis, Corpus, bibRecord, 000B48

Spécifications de services : une approche avec B

Identifieur interne : 000B48 ( PascalFrancis/Corpus ); précédent : 000B47; suivant : 000B49

Spécifications de services : une approche avec B

Auteurs : B. Mermet ; D. Mery ; D. Samborski

Source :

TSI. Technique et science informatiques [ 0752-4072 ] ; 1998.

RBID : Pascal:99-0095561

Descripteurs français

Pascal (Inist)
- Système réparti, Télécommunication, Génie logiciel, Spécification formelle, Service, Méthode B.

English descriptors

KwdEn :
- B method, Distributed system, Formal specification, Service, Software engineering, Telecommunication.

Abstract

Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.

Notice en format standard (ISO 2709)

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

A01	`01`	`1`		`@0 0752-4072`
A02	`01`			`@0 TTSIDJ`
A03		`1`		`@0 TSI, Tech. sci. inform.`
A05				`@2 17`
A06				`@2 9`
A08	`01`	`1`	`FRE`	`@1 Spécifications de services : une approche avec B`
A09	`01`	`1`	`FRE`	`@1 Approches formelles dans l'assistance au développement de logiciels`
A11	`01`	`1`		`@1 MERMET (B.)`
A11	`02`	`1`		`@1 MERY (D.)`
A11	`03`	`1`		`@1 SAMBORSKI (D.)`
A14	`01`			`@1 UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut.`
A18	`01`	`1`		`@1 Groupe ADER «Développement de Spécifications et de programmes» @3 FRA @9 patr.`
A18	`02`	`1`		`@1 Groupe FAC «Formalisation d'Activités Concurrentes» @3 FRA @9 patr.`
A20				`@1 1157-1180`
A21				`@1 1998`
A23	`01`			`@0 FRE`
A24	`01`			`@0 eng`
A43	`01`			`@1 INIST @2 19593 @5 354000072963050050`
A44				`@0 0000 @1 © 1999 INIST-CNRS. All rights reserved.`
A45				`@0 1 p.1/4`
A47	`01`	`1`		`@0 99-0095561`
A60				`@1 P @2 C`
A61				`@0 A`
A64		`1`		`@0 TSI. Technique et science informatiques`
A66	`01`			`@0 FRA`
A68	`01`	`1`	`ENG`	`@1 Service specifications using the B method`
C01	`01`		`FRE`	@0 Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.
C02	`01`	`X`		`@0 001D02B09`
C02	`02`	`X`		`@0 001D02B04`
C03	`01`	`X`	`FRE`	`@0 Système réparti @5 01`
C03	`01`	`X`	`ENG`	`@0 Distributed system @5 01`
C03	`01`	`X`	`SPA`	`@0 Sistema repartido @5 01`
C03	`02`	`X`	`FRE`	`@0 Télécommunication @5 02`
C03	`02`	`X`	`ENG`	`@0 Telecommunication @5 02`
C03	`02`	`X`	`GER`	`@0 Nachrichtentechnik @5 02`
C03	`02`	`X`	`SPA`	`@0 Telecomunicación @5 02`
C03	`03`	`X`	`FRE`	`@0 Génie logiciel @5 03`
C03	`03`	`X`	`ENG`	`@0 Software engineering @5 03`
C03	`03`	`X`	`SPA`	`@0 Ingeniería logiciel @5 03`
C03	`04`	`X`	`FRE`	`@0 Spécification formelle @5 04`
C03	`04`	`X`	`ENG`	`@0 Formal specification @5 04`
C03	`04`	`X`	`SPA`	`@0 Especificación formal @5 04`
C03	`05`	`X`	`FRE`	`@0 Service @5 05`
C03	`05`	`X`	`ENG`	`@0 Service @5 05`
C03	`05`	`X`	`SPA`	`@0 Servicio @5 05`
C03	`06`	`X`	`FRE`	`@0 Méthode B @4 CD @5 96`
C03	`06`	`X`	`ENG`	`@0 B method @4 CD @5 96`
N21				`@1 053`

A30	`01`	`1`	`FRE`	`@1 AFADL'97. Atelier @2 1 @3 Toulouse FRA @4 1997-05`

Format Inist (serveur)

NO :	PASCAL 99-0095561 INIST
FT :	Spécifications de services : une approche avec B
ET :	(Service specifications using the B method)
AU :	MERMET (B.); MERY (D.); SAMBORSKI (D.)
AF :	UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut., 3 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	TSI. Technique et science informatiques; ISSN 0752-4072; Coden TTSIDJ; France; Da. 1998; Vol. 17; No. 9; Pp. 1157-1180; Abs. anglais; Bibl. 1 p.1/4
LA :	Français
FA :	Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.
CC :	001D02B09; 001D02B04
FD :	Système réparti; Télécommunication; Génie logiciel; Spécification formelle; Service; Méthode B
ED :	Distributed system; Telecommunication; Software engineering; Formal specification; Service; B method
GD :	Nachrichtentechnik
SD :	Sistema repartido; Telecomunicación; Ingeniería logiciel; Especificación formal; Servicio
LO :	INIST-19593.354000072963050050
ID :	99-0095561

Links to Exploration step

Pascal:99-0095561

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Spécifications de services : une approche avec B</title>
<author><name sortKey="Mermet, B" sort="Mermet, B" uniqKey="Mermet B" first="B." last="Mermet">B. Mermet</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Samborski, D" sort="Samborski, D" uniqKey="Samborski D" first="D." last="Samborski">D. Samborski</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">99-0095561</idno>
<date when="1998">1998</date>
<idno type="stanalyst">PASCAL 99-0095561 INIST</idno>
<idno type="RBID">Pascal:99-0095561</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000B48</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Spécifications de services : une approche avec B</title>
<author><name sortKey="Mermet, B" sort="Mermet, B" uniqKey="Mermet B" first="B." last="Mermet">B. Mermet</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Samborski, D" sort="Samborski, D" uniqKey="Samborski D" first="D." last="Samborski">D. Samborski</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">TSI. Technique et science informatiques</title>
<title level="j" type="abbreviated">TSI, Tech. sci. inform.</title>
<idno type="ISSN">0752-4072</idno>
<imprint><date when="1998">1998</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">TSI. Technique et science informatiques</title>
<title level="j" type="abbreviated">TSI, Tech. sci. inform.</title>
<idno type="ISSN">0752-4072</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>B method</term>
<term>Distributed system</term>
<term>Formal specification</term>
<term>Service</term>
<term>Software engineering</term>
<term>Telecommunication</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Système réparti</term>
<term>Télécommunication</term>
<term>Génie logiciel</term>
<term>Spécification formelle</term>
<term>Service</term>
<term>Méthode B</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="fr">Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0752-4072</s0>
</fA01>
<fA02 i1="01"><s0>TTSIDJ</s0>
</fA02>
<fA03 i2="1"><s0>TSI, Tech. sci. inform.</s0>
</fA03>
<fA05><s2>17</s2>
</fA05>
<fA06><s2>9</s2>
</fA06>
<fA08 i1="01" i2="1" l="FRE"><s1>Spécifications de services : une approche avec B</s1>
</fA08>
<fA09 i1="01" i2="1" l="FRE"><s1>Approches formelles dans l'assistance au développement de logiciels</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>MERMET (B.)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>MERY (D.)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>SAMBORSKI (D.)</s1>
</fA11>
<fA14 i1="01"><s1>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14>
<fA18 i1="01" i2="1"><s1>Groupe ADER «Développement de Spécifications et de programmes»</s1>
<s3>FRA</s3>
<s9>patr.</s9>
</fA18>
<fA18 i1="02" i2="1"><s1>Groupe FAC «Formalisation d'Activités Concurrentes»</s1>
<s3>FRA</s3>
<s9>patr.</s9>
</fA18>
<fA20><s1>1157-1180</s1>
</fA20>
<fA21><s1>1998</s1>
</fA21>
<fA23 i1="01"><s0>FRE</s0>
</fA23>
<fA24 i1="01"><s0>eng</s0>
</fA24>
<fA43 i1="01"><s1>INIST</s1>
<s2>19593</s2>
<s5>354000072963050050</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 1999 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>1 p.1/4</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>99-0095561</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i2="1"><s0>TSI. Technique et science informatiques</s0>
</fA64>
<fA66 i1="01"><s0>FRA</s0>
</fA66>
<fA68 i1="01" i2="1" l="ENG"><s1>Service specifications using the B method</s1>
</fA68>
<fC01 i1="01" l="FRE"><s0>Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B04</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Système réparti</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Distributed system</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Sistema repartido</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Télécommunication</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Telecommunication</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="GER"><s0>Nachrichtentechnik</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Telecomunicación</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Génie logiciel</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Software engineering</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Ingeniería logiciel</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Spécification formelle</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Formal specification</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Especificación formal</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Service</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Service</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Servicio</s0>
<s5>05</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Méthode B</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>B method</s0>
<s4>CD</s4>
<s5>96</s5>
</fC03>
<fN21><s1>053</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="FRE"><s1>AFADL'97. Atelier</s1>
<s2>1</s2>
<s3>Toulouse FRA</s3>
<s4>1997-05</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 99-0095561 INIST</NO>
<FT>Spécifications de services : une approche avec B</FT>
<ET>(Service specifications using the B method)</ET>
<AU>MERMET (B.); MERY (D.); SAMBORSKI (D.)</AU>
<AF>UMR n°7503, LORIA, Université Henri Poincaré Nancy I, Campus scientifique, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut., 3 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>TSI. Technique et science informatiques; ISSN 0752-4072; Coden TTSIDJ; France; Da. 1998; Vol. 17; No. 9; Pp. 1157-1180; Abs. anglais; Bibl. 1 p.1/4</SO>
<LA>Français</LA>
<FA>Nous présentons une étude de cas réalisée en B concernant la spécification de services de télécommunications et l'utilisation de cette méthode pour la gestion d'interactions possibles entre de tels services. La composition des services conduit à des interactions et la méthode B est utilisée pour les développer, les composer et établir la présence ou l'absence d'interaction au niveau de la spécification. Le prouveur et l'animateur se révèlent être des outils très utiles non seulement pour détecter les interactions, mais aussi pour aider l'utilisateur à les résoudre. Nous illustrons la démarche par des exemples de l'ensemble de capacités 1 CS 1 de l'Union Internationale des Télécommunications, et nous donnons quelques statistiques sur la performance des outils utilisés.</FA>
<CC>001D02B09; 001D02B04</CC>
<FD>Système réparti; Télécommunication; Génie logiciel; Spécification formelle; Service; Méthode B</FD>
<ED>Distributed system; Telecommunication; Software engineering; Formal specification; Service; B method</ED>
<GD>Nachrichtentechnik</GD>
<SD>Sistema repartido; Telecomunicación; Ingeniería logiciel; Especificación formal; Servicio</SD>
<LO>INIST-19593.354000072963050050</LO>
<ID>99-0095561</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 000B48 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000B48 | 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:99-0095561
   |texte=   Spécifications de services : une approche avec B
}}

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

Spécifications de services : une approche avec B

Spécifications de services : une approche avec B

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