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 : 000209Utilisation de B pour l'aide à la spécification d'un système de diagnostic
Auteurs : Dominique Cansell [France] ; Jacques Jaray [France]Source :
Descripteurs français
- Pascal (Inist)
English descriptors
- KwdEn :
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.
pA |
|
---|
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-0580630Le 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
Ou
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. | ![]() |