InforLorV4, PascalFrancis, Curation, bibRecord, 000208

Utilisation de B pour l'aide à la spécification d'un système de diagnostic

Identifieur interne : 000208 ( PascalFrancis/Curation ); précédent : 000207; suivant : 000209

Utilisation de B pour l'aide à la spécification d'un système de diagnostic

Auteurs : Dominique Cansell [France] ; Jacques Jaray [France]

Source :

RBID : Pascal:02-0580630

Descripteurs français

Pascal (Inist)
- Diagnostic, Dépendance, Défaillance, Cahier charge, Satisfaction, Développement logiciel, Méthode B, Spécification système, Système diagnostic.

English descriptors

KwdEn :
- Contract specifications, Dependence, Diagnosis, Failures, Satisfaction, Software development.

Abstract

L'article présente une manière de construire un algorithme de diagnostic d'un système critique. Son rôle est de surveiller les défaillances pouvant être observées sur des organes, à l'aide de capteurs. L'occurrence d'une défaillance nécessite le passage immédiat dans un mode adéquat. Le problème est rendu difficile par la nature même des informations provenant des capteurs et par la dépendance entre les défaillances possibles. Le nombre de situations étant assez grand, il n'est pas si facile de construire un algorithme correct de gestion des défaillances. Pour ce faire nous sommes partis d'un cahier des charges succinct et avons construit un premier modèle B. C'est l'échec de la preuve qui a mis en évidence une incomplétude du cahier des charges et qui nous a permis d'étudier avec le client la correction à apporter au cahier des charges. Le procédé a été répété jusqu'à l'obtention d'un modèle satisfaisant.

A08	`01`	`1`	`FRE`	`@1 Utilisation de B pour l'aide à la spécification d'un système de diagnostic`
A09	`01`	`1`	`FRE`	`@1 AFADL'2001 : approches formelles dans l'assistance au développement de logiciels : Nancy, 11-13 juin 2001`
A11	`01`	`1`		`@1 CANSELL (Dominique)`
A11	`02`	`1`		`@1 JARAY (Jacques)`
A14	`01`			`@1 UMR n° 7503 LORIA, Université de Metz @3 FRA @Z 1 aut.`
A14	`02`			`@1 UMR n° 7503 LORIA, INPL-Ecole des Mines de Nancy @3 FRA @Z 2 aut.`
A18	`01`	`1`		`@1 CNRS. Laboratoire lorrain de recherche en informatique et ses applications @2 Vandoeuvre-lès-Nancy @3 FRA @9 patr.`
A18	`02`	`1`		`@1 Groupe ADER @3 FRA @9 patr.`
A20				`@1 67-81`
A21				`@1 2001`
A23	`01`			`@0 FRE`
A30	`01`	`1`	`FRE`	`@1 Approches formelles dans l'assistance au développement de logiciels. Atelier @2 4 @3 Nancy FRA @4 2001-06-11`
A43	`01`			`@1 INIST @2 Y 34089 @5 354000108428710050`
A44				`@0 0000 @1 © 2002 INIST-CNRS. All rights reserved.`
A45				`@0 12 ref.`
A47	`01`	`1`		`@0 02-0580630`
A60				`@1 C`
A61				`@0 A`
A66	`01`			`@0 FRA`
A68	`01`	`1`	`ENG`	`@1 B method uses to aids of diagnostic system specification`
C01	`01`		`FRE`	@0 L'article présente une manière de construire un algorithme de diagnostic d'un système critique. Son rôle est de surveiller les défaillances pouvant être observées sur des organes, à l'aide de capteurs. L'occurrence d'une défaillance nécessite le passage immédiat dans un mode adéquat. Le problème est rendu difficile par la nature même des informations provenant des capteurs et par la dépendance entre les défaillances possibles. Le nombre de situations étant assez grand, il n'est pas si facile de construire un algorithme correct de gestion des défaillances. Pour ce faire nous sommes partis d'un cahier des charges succinct et avons construit un premier modèle B. C'est l'échec de la preuve qui a mis en évidence une incomplétude du cahier des charges et qui nous a permis d'étudier avec le client la correction à apporter au cahier des charges. Le procédé a été répété jusqu'à l'obtention d'un modèle satisfaisant.
C02	`01`	`X`		`@0 001D02B09`
C02	`02`	`X`		`@0 001D02B10`
C03	`01`	`X`	`FRE`	`@0 Diagnostic @5 01`
C03	`01`	`X`	`ENG`	`@0 Diagnosis @5 01`
C03	`01`	`X`	`SPA`	`@0 Diagnóstico @5 01`
C03	`02`	`X`	`FRE`	`@0 Dépendance @5 02`
C03	`02`	`X`	`ENG`	`@0 Dependence @5 02`
C03	`02`	`X`	`SPA`	`@0 Dependencia @5 02`
C03	`03`	`X`	`FRE`	`@0 Défaillance @5 03`
C03	`03`	`X`	`ENG`	`@0 Failures @5 03`
C03	`03`	`X`	`SPA`	`@0 Fallo @5 03`
C03	`04`	`X`	`FRE`	`@0 Cahier charge @5 04`
C03	`04`	`X`	`ENG`	`@0 Contract specifications @5 04`
C03	`04`	`X`	`SPA`	`@0 Pliego condiciones @5 04`
C03	`05`	`X`	`FRE`	`@0 Satisfaction @5 05`
C03	`05`	`X`	`ENG`	`@0 Satisfaction @5 05`
C03	`05`	`X`	`SPA`	`@0 Satisfacción @5 05`
C03	`06`	`X`	`FRE`	`@0 Développement logiciel @5 06`
C03	`06`	`X`	`ENG`	`@0 Software development @5 06`
C03	`06`	`X`	`SPA`	`@0 Desarrollo logicial @5 06`
C03	`07`	`X`	`FRE`	`@0 Méthode B @4 INC @5 82`
C03	`08`	`X`	`FRE`	`@0 Spécification système @4 INC @5 83`
C03	`09`	`X`	`FRE`	`@0 Système diagnostic @4 INC @5 84`
N21				`@1 343`
N82				`@1 PSI`

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

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

Links to Exploration step

Pascal:02-0580630

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Utilisation de B pour l'aide à la spécification d'un système de diagnostic</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>UMR n° 7503 LORIA, Université de Metz</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Jaray, Jacques" sort="Jaray, Jacques" uniqKey="Jaray J" first="Jacques" last="Jaray">Jacques Jaray</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>UMR n° 7503 LORIA, INPL-Ecole des Mines de Nancy</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">02-0580630</idno>
<date when="2001">2001</date>
<idno type="stanalyst">PASCAL 02-0580630 INIST</idno>
<idno type="RBID">Pascal:02-0580630</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000844</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000208</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Utilisation de B pour l'aide à la spécification d'un système de diagnostic</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>UMR n° 7503 LORIA, Université de Metz</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
<author><name sortKey="Jaray, Jacques" sort="Jaray, Jacques" uniqKey="Jaray J" first="Jacques" last="Jaray">Jacques Jaray</name>
<affiliation wicri:level="1"><inist:fA14 i1="02"><s1>UMR n° 7503 LORIA, INPL-Ecole des Mines de Nancy</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
</affiliation>
</author>
</analytic>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Contract specifications</term>
<term>Dependence</term>
<term>Diagnosis</term>
<term>Failures</term>
<term>Satisfaction</term>
<term>Software development</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Diagnostic</term>
<term>Dépendance</term>
<term>Défaillance</term>
<term>Cahier charge</term>
<term>Satisfaction</term>
<term>Développement logiciel</term>
<term>Méthode B</term>
<term>Spécification système</term>
<term>Système diagnostic</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="fr">L'article présente une manière de construire un algorithme de diagnostic d'un système critique. Son rôle est de surveiller les défaillances pouvant être observées sur des organes, à l'aide de capteurs. L'occurrence d'une défaillance nécessite le passage immédiat dans un mode adéquat. Le problème est rendu difficile par la nature même des informations provenant des capteurs et par la dépendance entre les défaillances possibles. Le nombre de situations étant assez grand, il n'est pas si facile de construire un algorithme correct de gestion des défaillances. Pour ce faire nous sommes partis d'un cahier des charges succinct et avons construit un premier modèle B. C'est l'échec de la preuve qui a mis en évidence une incomplétude du cahier des charges et qui nous a permis d'étudier avec le client la correction à apporter au cahier des charges. Le procédé a été répété jusqu'à l'obtention d'un modèle satisfaisant.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA08 i1="01" i2="1" l="FRE"><s1>Utilisation de B pour l'aide à la spécification d'un système de diagnostic</s1>
</fA08>
<fA09 i1="01" i2="1" l="FRE"><s1>AFADL'2001 : approches formelles dans l'assistance au développement de logiciels : Nancy, 11-13 juin 2001 </s1>
</fA09>
<fA11 i1="01" i2="1"><s1>CANSELL (Dominique)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>JARAY (Jacques)</s1>
</fA11>
<fA14 i1="01"><s1>UMR n° 7503 LORIA, Université de Metz</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>UMR n° 7503 LORIA, INPL-Ecole des Mines de Nancy</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</fA14>
<fA18 i1="01" i2="1"><s1>CNRS. Laboratoire lorrain de recherche en informatique et ses applications</s1>
<s2>Vandoeuvre-lès-Nancy</s2>
<s3>FRA</s3>
<s9>patr.</s9>
</fA18>
<fA18 i1="02" i2="1"><s1>Groupe ADER</s1>
<s3>FRA</s3>
<s9>patr.</s9>
</fA18>
<fA20><s1>67-81</s1>
</fA20>
<fA21><s1>2001</s1>
</fA21>
<fA23 i1="01"><s0>FRE</s0>
</fA23>
<fA30 i1="01" i2="1" l="FRE"><s1>Approches formelles dans l'assistance au développement de logiciels. Atelier</s1>
<s2>4</s2>
<s3>Nancy FRA</s3>
<s4>2001-06-11</s4>
</fA30>
<fA43 i1="01"><s1>INIST</s1>
<s2>Y 34089</s2>
<s5>354000108428710050</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2002 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>12 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>02-0580630</s0>
</fA47>
<fA60><s1>C</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA66 i1="01"><s0>FRA</s0>
</fA66>
<fA68 i1="01" i2="1" l="ENG"><s1>B method uses to aids of diagnostic system specification</s1>
</fA68>
<fC01 i1="01" l="FRE"><s0>L'article présente une manière de construire un algorithme de diagnostic d'un système critique. Son rôle est de surveiller les défaillances pouvant être observées sur des organes, à l'aide de capteurs. L'occurrence d'une défaillance nécessite le passage immédiat dans un mode adéquat. Le problème est rendu difficile par la nature même des informations provenant des capteurs et par la dépendance entre les défaillances possibles. Le nombre de situations étant assez grand, il n'est pas si facile de construire un algorithme correct de gestion des défaillances. Pour ce faire nous sommes partis d'un cahier des charges succinct et avons construit un premier modèle B. C'est l'échec de la preuve qui a mis en évidence une incomplétude du cahier des charges et qui nous a permis d'étudier avec le client la correction à apporter au cahier des charges. Le procédé a été répété jusqu'à l'obtention d'un modèle satisfaisant.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02>
<fC02 i1="02" i2="X"><s0>001D02B10</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Diagnostic</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Diagnosis</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Diagnóstico</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Dépendance</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Dependence</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Dependencia</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Défaillance</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Failures</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Fallo</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Cahier charge</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Contract specifications</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Pliego condiciones</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="X" l="FRE"><s0>Satisfaction</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="ENG"><s0>Satisfaction</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="X" l="SPA"><s0>Satisfacción</s0>
<s5>05</s5>
</fC03>
<fC03 i1="06" i2="X" l="FRE"><s0>Développement logiciel</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="ENG"><s0>Software development</s0>
<s5>06</s5>
</fC03>
<fC03 i1="06" i2="X" l="SPA"><s0>Desarrollo logicial</s0>
<s5>06</s5>
</fC03>
<fC03 i1="07" i2="X" l="FRE"><s0>Méthode B</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03>
<fC03 i1="08" i2="X" l="FRE"><s0>Spécification système</s0>
<s4>INC</s4>
<s5>83</s5>
</fC03>
<fC03 i1="09" i2="X" l="FRE"><s0>Système diagnostic</s0>
<s4>INC</s4>
<s5>84</s5>
</fC03>
<fN21><s1>343</s1>
</fN21>
<fN82><s1>PSI</s1>
</fN82>
</pA>
</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 000208 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000208 | 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:02-0580630
   |texte=   Utilisation de B pour l'aide à la spécification d'un système de diagnostic
}}

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

Utilisation de B pour l'aide à la spécification d'un système de diagnostic

Utilisation de B pour l'aide à la spécification d'un système de diagnostic

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