Construction sûre de systèmes électroniques
Identifieur interne : 000641 ( PascalFrancis/Corpus ); précédent : 000640; suivant : 000642Construction sûre de systèmes électroniques
Auteurs : Dominique Cansell ; Stefan Hallerstede ; Yann ZimmermannSource :
- Génie logiciel : (1995) [ 1265-1397 ] ; 2004.
Descripteurs français
- Pascal (Inist)
English descriptors
Abstract
Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.
Notice en format standard (ISO 2709)
Pour connaître la documentation sur le format Inist Standard.
pA |
|
---|
Format Inist (serveur)
NO : | PASCAL 04-0431807 INIST |
---|---|
FT : | Construction sûre de systèmes électroniques |
ET : | (Reliable design of electronic systems) |
AU : | CANSELL (Dominique); HALLERSTEDE (Stefan); ZIMMERMANN (Yann) |
AF : | Université de Nancy, LORIA/France (1 aut.); KeesDA/Inconnu (2 aut.); KeesDA & LDRIA/Inconnu (3 aut.) |
DT : | Publication en série; Niveau analytique |
SO : | Génie logiciel : (1995); ISSN 1265-1397; France; Da. 2004; No. 69; Pp. 38-44; Bibl. 10 ref. |
LA : | Français |
FA : | Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'. |
CC : | 001D02B09 |
FD : | Méthode formelle; Vérification programme; Système construction; Méthode raffinement |
ED : | Formal method; Program verification; Construction system; Refinement method |
SD : | Método formal; Verificación programa; Sistema construcción; Método afinamiento |
LO : | INIST-21864.354000110544350060 |
ID : | 04-0431807 |
Links to Exploration step
Pascal:04-0431807Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Construction sûre de systèmes électroniques</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>Université de Nancy, LORIA</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Hallerstede, Stefan" sort="Hallerstede, Stefan" uniqKey="Hallerstede S" first="Stefan" last="Hallerstede">Stefan Hallerstede</name>
<affiliation><inist:fA14 i1="02"><s1>KeesDA</s1>
<s3>INC</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Zimmermann, Yann" sort="Zimmermann, Yann" uniqKey="Zimmermann Y" first="Yann" last="Zimmermann">Yann Zimmermann</name>
<affiliation><inist:fA14 i1="03"><s1>KeesDA & LDRIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">04-0431807</idno>
<date when="2004">2004</date>
<idno type="stanalyst">PASCAL 04-0431807 INIST</idno>
<idno type="RBID">Pascal:04-0431807</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000641</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Construction sûre de systèmes électroniques</title>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation><inist:fA14 i1="01"><s1>Université de Nancy, LORIA</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Hallerstede, Stefan" sort="Hallerstede, Stefan" uniqKey="Hallerstede S" first="Stefan" last="Hallerstede">Stefan Hallerstede</name>
<affiliation><inist:fA14 i1="02"><s1>KeesDA</s1>
<s3>INC</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Zimmermann, Yann" sort="Zimmermann, Yann" uniqKey="Zimmermann Y" first="Yann" last="Zimmermann">Yann Zimmermann</name>
<affiliation><inist:fA14 i1="03"><s1>KeesDA & LDRIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Génie logiciel : (1995)</title>
<title level="j" type="abbreviated">Génie logiciel : (1995)</title>
<idno type="ISSN">1265-1397</idno>
<imprint><date when="2004">2004</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Génie logiciel : (1995)</title>
<title level="j" type="abbreviated">Génie logiciel : (1995)</title>
<idno type="ISSN">1265-1397</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Construction system</term>
<term>Formal method</term>
<term>Program verification</term>
<term>Refinement method</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Méthode formelle</term>
<term>Vérification programme</term>
<term>Système construction</term>
<term>Méthode raffinement</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="fr">Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>1265-1397</s0>
</fA01>
<fA03 i2="1"><s0>Génie logiciel : (1995)</s0>
</fA03>
<fA06><s2>69</s2>
</fA06>
<fA08 i1="01" i2="1" l="FRE"><s1>Construction sûre de systèmes électroniques</s1>
</fA08>
<fA11 i1="01" i2="1"><s1>CANSELL (Dominique)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>HALLERSTEDE (Stefan)</s1>
</fA11>
<fA11 i1="03" i2="1"><s1>ZIMMERMANN (Yann)</s1>
</fA11>
<fA14 i1="01"><s1>Université de Nancy, LORIA</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA14>
<fA14 i1="02"><s1>KeesDA</s1>
<s3>INC</s3>
<sZ>2 aut.</sZ>
</fA14>
<fA14 i1="03"><s1>KeesDA & LDRIA</s1>
<s3>INC</s3>
<sZ>3 aut.</sZ>
</fA14>
<fA20><s1>38-44</s1>
</fA20>
<fA21><s1>2004</s1>
</fA21>
<fA23 i1="01"><s0>FRE</s0>
</fA23>
<fA43 i1="01"><s1>INIST</s1>
<s2>21864</s2>
<s5>354000110544350060</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 2004 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>10 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>04-0431807</s0>
</fA47>
<fA60><s1>P</s1>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i1="01" i2="1"><s0>Génie logiciel : (1995)</s0>
</fA64>
<fA66 i1="01"><s0>FRA</s0>
</fA66>
<fA68 i1="01" i2="1" l="ENG"><s1>Reliable design of electronic systems</s1>
</fA68>
<fA99><s0>3 notes</s0>
</fA99>
<fC01 i1="01" l="FRE"><s0>Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Méthode formelle</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>Formal method</s0>
<s5>06</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Método formal</s0>
<s5>06</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Vérification programme</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Program verification</s0>
<s5>07</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Verificación programa</s0>
<s5>07</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Système construction</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Construction system</s0>
<s5>18</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Sistema construcción</s0>
<s5>18</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Méthode raffinement</s0>
<s5>23</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>Refinement method</s0>
<s5>23</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Método afinamiento</s0>
<s5>23</s5>
</fC03>
<fN21><s1>243</s1>
</fN21>
<fN44 i1="01"><s1>PSI</s1>
</fN44>
<fN82><s1>PSI</s1>
</fN82>
</pA>
</standard>
<server><NO>PASCAL 04-0431807 INIST</NO>
<FT>Construction sûre de systèmes électroniques</FT>
<ET>(Reliable design of electronic systems)</ET>
<AU>CANSELL (Dominique); HALLERSTEDE (Stefan); ZIMMERMANN (Yann)</AU>
<AF>Université de Nancy, LORIA/France (1 aut.); KeesDA/Inconnu (2 aut.); KeesDA & LDRIA/Inconnu (3 aut.)</AF>
<DT>Publication en série; Niveau analytique</DT>
<SO>Génie logiciel : (1995); ISSN 1265-1397; France; Da. 2004; No. 69; Pp. 38-44; Bibl. 10 ref.</SO>
<LA>Français</LA>
<FA>Le développement de systèmes à l'aide du raffinement est une méthode formelle qui permet de gérer la complexité d'un système et de sa preuve de correction en permettant l'introduction des détails du système pas à pas À partir d'un système abstrait, chaque pas du raffinement est prouvé correct jusqu'au niveau d'implantation. La méthode B est basée sur le raffinement, mais elle aide aussi à gérer les obligations de preuve qui se présentent à chaque pas. La méthode B est l'une des méthodes qui possèdent le plus d'outils support pour être utilisée en pratique. Les systèmes électroniques deviennent de plus en plus complexes, l'approche traditionnelle qui consiste à garantir la correction parla simulation ne suffit plus. Par ailleurs, les systèmes électroniques sont de plus en plus présents dans les systèmes de toute nature et l'exigence en qualité est de plus en plus forte. Les méthodes formelles sont les seules à pouvoir faire face à cette complexité croissante. Nous présentons dans cet article comment la méthode B peut être utilisée pour la conception des systèmes électroniques'.</FA>
<CC>001D02B09</CC>
<FD>Méthode formelle; Vérification programme; Système construction; Méthode raffinement</FD>
<ED>Formal method; Program verification; Construction system; Refinement method</ED>
<SD>Método formal; Verificación programa; Sistema construcción; Método afinamiento</SD>
<LO>INIST-21864.354000110544350060</LO>
<ID>04-0431807</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 000641 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000641 | 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:04-0431807 |texte= Construction sûre de systèmes électroniques }}
![]() | This area was generated with Dilib version V0.6.33. | ![]() |