Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B
Identifieur interne :
000664 ( PascalFrancis/Curation );
précédent :
000663;
suivant :
000665
Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B
Auteurs : Akram Idani [
France] ;
Yves Ledru [
France] ;
Didier Bert [
France]
Source :
-
TSI. Technique et science informatiques [ 0752-4072 ] ; 2007.
RBID : Pascal:08-0014543
Descripteurs français
English descriptors
Abstract
Formal methods are nowadays one of the most rigorous ways to develop software and model systems. But their notations are complex which prevents their adoption. In fact, formal models remain difficult to read when they are not well documented. In a previous work we proposed a reverse-engineering framework which allows to graphically document B specifications by automatically deriving structural UML views. Our approach is based on a concept formation technique. In this paper, we formalize our algorithm and we prove that the generated context models satisfy a set of pertinency criteria. Finally, we show how our technique can be used in order to take refinements into account.
| pA |
| A01 | 01 | 1 | | @0 0752-4072 |
|---|
| A02 | 01 | | | @0 TTSIDJ |
|---|
| A03 | | 1 | | @0 TSI, Tech. sci. inform. |
|---|
| A05 | | | | @2 26 |
|---|
| A06 | | | | @2 7 |
|---|
| A08 | 01 | 1 | FRE | @1 Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B |
|---|
| A09 | 01 | 1 | FRE | @1 Approches formelles pour le développement de logiciels : AFADL 2006 |
|---|
| A11 | 01 | 1 | | @1 IDANI (Akram) |
|---|
| A11 | 02 | 1 | | @1 LEDRU (Yves) |
|---|
| A11 | 03 | 1 | | @1 BERT (Didier) |
|---|
| A12 | 01 | 1 | | @1 SOUQUIERES (Jeanine) @9 ed. |
|---|
| A14 | 01 | | | @1 Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72 @2 38402 St Martin d'Hères @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A14 | 02 | | | @1 Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS @3 FRA |
|---|
| A15 | 01 | | | @1 LORIA - Université de Nancy 2 @3 FRA @Z 1 aut. |
|---|
| A18 | 01 | 1 | | @1 CNRS. GDR Informatique Mathématique. Atelier Approches Formelles dans l'Assistance au Développement de Logiciels @3 FRA @9 org-cong. |
|---|
| A20 | | | | @1 819-851 |
|---|
| A21 | | | | @1 2007 |
|---|
| A23 | 01 | | | @0 FRE |
|---|
| A24 | 01 | | | @0 eng |
|---|
| A43 | 01 | | | @1 INIST @2 19593 @5 354000160939580020 |
|---|
| A44 | | | | @0 0000 @1 © 2008 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 2 p. |
|---|
| A47 | 01 | 1 | | @0 08-0014543 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 TSI. Technique et science informatiques |
|---|
| A66 | 01 | | | @0 FRA |
|---|
| C01 | 01 | | ENG | @0 Formal methods are nowadays one of the most rigorous ways to develop software and model systems. But their notations are complex which prevents their adoption. In fact, formal models remain difficult to read when they are not well documented. In a previous work we proposed a reverse-engineering framework which allows to graphically document B specifications by automatically deriving structural UML views. Our approach is based on a concept formation technique. In this paper, we formalize our algorithm and we prove that the generated context models satisfy a set of pertinency criteria. Finally, we show how our technique can be used in order to take refinements into account. |
|---|
| C02 | 01 | X | | @0 001D02B09 |
|---|
| C03 | 01 | X | FRE | @0 Développement logiciel @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Software development @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Desarrollo logicial @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Langage modélisation unifié @5 06 |
|---|
| C03 | 02 | X | ENG | @0 Unified modelling language @5 06 |
|---|
| C03 | 02 | X | SPA | @0 Lenguaje UML @5 06 |
|---|
| C03 | 03 | X | FRE | @0 Méthode formelle @5 07 |
|---|
| C03 | 03 | X | ENG | @0 Formal method @5 07 |
|---|
| C03 | 03 | X | SPA | @0 Método formal @5 07 |
|---|
| C03 | 04 | X | FRE | @0 Spécification formelle @5 08 |
|---|
| C03 | 04 | X | ENG | @0 Formal specification @5 08 |
|---|
| C03 | 04 | X | SPA | @0 Especificación formal @5 08 |
|---|
| C03 | 05 | X | FRE | @0 Rétroingénierie @5 18 |
|---|
| C03 | 05 | X | ENG | @0 Reverse engineering @5 18 |
|---|
| C03 | 05 | X | SPA | @0 Ingeniera inversa @5 18 |
|---|
| C03 | 06 | X | FRE | @0 Sémantique @5 19 |
|---|
| C03 | 06 | X | ENG | @0 Semantics @5 19 |
|---|
| C03 | 06 | X | SPA | @0 Semántica @5 19 |
|---|
| C03 | 07 | X | FRE | @0 Analyse conceptuelle @5 20 |
|---|
| C03 | 07 | X | ENG | @0 Conceptual analysis @5 20 |
|---|
| C03 | 07 | X | SPA | @0 Análisis conceptual @5 20 |
|---|
| C03 | 08 | X | FRE | @0 Modélisation @5 23 |
|---|
| C03 | 08 | X | ENG | @0 Modeling @5 23 |
|---|
| C03 | 08 | X | SPA | @0 Modelización @5 23 |
|---|
| C03 | 09 | X | FRE | @0 Méthode raffinement @5 24 |
|---|
| C03 | 09 | X | ENG | @0 Refinement method @5 24 |
|---|
| C03 | 09 | X | SPA | @0 Método afinamiento @5 24 |
|---|
| C03 | 10 | X | FRE | @0 . @4 INC @5 82 |
|---|
| N21 | | | | @1 009 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | FRE | @1 Rencontres de l'atelier AFADL @2 7 @3 Paris FRA @4 2006-03 |
|---|
|
|---|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000361
Links to Exploration step
Pascal:08-0014543
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="fr" level="a">Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B</title>
<author><name sortKey="Idani, Akram" sort="Idani, Akram" uniqKey="Idani A" first="Akram" last="Idani">Akram Idani</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS</s1>
<s3>FRA</s3>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Ledru, Yves" sort="Ledru, Yves" uniqKey="Ledru Y" first="Yves" last="Ledru">Yves Ledru</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Bert, Didier" sort="Bert, Didier" uniqKey="Bert D" first="Didier" last="Bert">Didier Bert</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">08-0014543</idno>
<date when="2007">2007</date>
<idno type="stanalyst">PASCAL 08-0014543 INIST</idno>
<idno type="RBID">Pascal:08-0014543</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000361</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000664</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="fr" level="a">Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B</title>
<author><name sortKey="Idani, Akram" sort="Idani, Akram" uniqKey="Idani A" first="Akram" last="Idani">Akram Idani</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><affiliation wicri:level="1"><inist:fA14 i1="02"><s1>Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS</s1>
<s3>FRA</s3>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Ledru, Yves" sort="Ledru, Yves" uniqKey="Ledru Y" first="Yves" last="Ledru">Yves Ledru</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><author><name sortKey="Bert, Didier" sort="Bert, Didier" uniqKey="Bert D" first="Didier" last="Bert">Didier Bert</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</inist:fA14><country>France</country>
</affiliation><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="2007">2007</date>
</imprint><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><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Conceptual analysis</term>
<term>Formal method</term>
<term>Formal specification</term>
<term>Modeling</term>
<term>Refinement method</term>
<term>Reverse engineering</term>
<term>Semantics</term>
<term>Software development</term>
<term>Unified modelling language</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Développement logiciel</term>
<term>Langage modélisation unifié</term>
<term>Méthode formelle</term>
<term>Spécification formelle</term>
<term>Rétroingénierie</term>
<term>Sémantique</term>
<term>Analyse conceptuelle</term>
<term>Modélisation</term>
<term>Méthode raffinement</term>
<term>.</term>
</keywords><front><div type="abstract" xml:lang="en">Formal methods are nowadays one of the most rigorous ways to develop software and model systems. But their notations are complex which prevents their adoption. In fact, formal models remain difficult to read when they are not well documented. In a previous work we proposed a reverse-engineering framework which allows to graphically document B specifications by automatically deriving structural UML views. Our approach is based on a concept formation technique. In this paper, we formalize our algorithm and we prove that the generated context models satisfy a set of pertinency criteria. Finally, we show how our technique can be used in order to take refinements into account.</div>
</front><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><fA08 i1="01" i2="1" l="FRE"><s1>Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements B</s1>
</fA08><fA09 i1="01" i2="1" l="FRE"><s1>Approches formelles pour le développement de logiciels : AFADL 2006</s1>
</fA09><fA11 i1="01" i2="1"><s1>IDANI (Akram)</s1>
</fA11><fA11 i1="02" i2="1"><s1>LEDRU (Yves)</s1>
</fA11><fA11 i1="03" i2="1"><s1>BERT (Didier)</s1>
</fA11><fA12 i1="01" i2="1"><s1>SOUQUIERES (Jeanine)</s1>
<s9>ed.</s9>
</fA12><fA14 i1="01"><s1>Laboratoire d'informatique de Grenoble (LIG), équipe VASCO 681 rue de la passerelle, domaine universitaire, BP 72</s1>
<s2>38402 St Martin d'Hères</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA14 i1="02"><s1>Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS</s1>
<s3>FRA</s3>
</fA14><fA15 i1="01"><s1>LORIA - Université de Nancy 2</s1>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
</fA15><fA18 i1="01" i2="1"><s1>CNRS. GDR Informatique Mathématique. Atelier Approches Formelles dans l'Assistance au Développement de Logiciels</s1>
<s3>FRA</s3>
<s9>org-cong.</s9>
</fA18><fA20><s1>819-851</s1>
</fA20><fA21><s1>2007</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>354000160939580020</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2008 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>2 p.</s0>
</fA45><fA47 i1="01" i2="1"><s0>08-0014543</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>TSI. Technique et science informatiques</s0>
</fA64><fA66 i1="01"><s0>FRA</s0>
</fA66><fC01 i1="01" l="ENG"><s0>Formal methods are nowadays one of the most rigorous ways to develop software and model systems. But their notations are complex which prevents their adoption. In fact, formal models remain difficult to read when they are not well documented. In a previous work we proposed a reverse-engineering framework which allows to graphically document B specifications by automatically deriving structural UML views. Our approach is based on a concept formation technique. In this paper, we formalize our algorithm and we prove that the generated context models satisfy a set of pertinency criteria. Finally, we show how our technique can be used in order to take refinements into account.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Développement logiciel</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Software development</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Desarrollo logicial</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Langage modélisation unifié</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Unified modelling language</s0>
<s5>06</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Lenguaje UML</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Méthode formelle</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Formal method</s0>
<s5>07</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Método formal</s0>
<s5>07</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Spécification formelle</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Formal specification</s0>
<s5>08</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Especificación formal</s0>
<s5>08</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Rétroingénierie</s0>
<s5>18</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Reverse engineering</s0>
<s5>18</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Ingeniera inversa</s0>
<s5>18</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Sémantique</s0>
<s5>19</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Semantics</s0>
<s5>19</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Semántica</s0>
<s5>19</s5>
</fC03><fC03 i1="07" i2="X" l="FRE"><s0>Analyse conceptuelle</s0>
<s5>20</s5>
</fC03><fC03 i1="07" i2="X" l="ENG"><s0>Conceptual analysis</s0>
<s5>20</s5>
</fC03><fC03 i1="07" i2="X" l="SPA"><s0>Análisis conceptual</s0>
<s5>20</s5>
</fC03><fC03 i1="08" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>23</s5>
</fC03><fC03 i1="08" i2="X" l="ENG"><s0>Modeling</s0>
<s5>23</s5>
</fC03><fC03 i1="08" i2="X" l="SPA"><s0>Modelización</s0>
<s5>23</s5>
</fC03><fC03 i1="09" i2="X" l="FRE"><s0>Méthode raffinement</s0>
<s5>24</s5>
</fC03><fC03 i1="09" i2="X" l="ENG"><s0>Refinement method</s0>
<s5>24</s5>
</fC03><fC03 i1="09" i2="X" l="SPA"><s0>Método afinamiento</s0>
<s5>24</s5>
</fC03><fC03 i1="10" i2="X" l="FRE"><s0>.</s0>
<s4>INC</s4>
<s5>82</s5>
</fC03><fN21><s1>009</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="FRE"><s1>Rencontres de l'atelier AFADL</s1>
<s2>7</s2>
<s3>Paris FRA</s3>
<s4>2006-03</s4>
</fA30>
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 000664 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000664 | 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:08-0014543
|texte= Approche formelle pour la dérivation de vues structurelles UML à partir de développements B : Formalisation, preuve et extension pour la prise en compte des raffinements 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 |  |
