InforLorV4, Main, Exploration, bibRecord, 004D44

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 : 004D44 ( Main/Exploration ); précédent : 004D43; suivant : 004D45

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

Pascal (Inist)
- Développement logiciel, Langage modélisation unifié, Méthode formelle, Spécification formelle, Rétroingénierie, Sémantique, Analyse conceptuelle, Modélisation, Méthode raffinement, ..

English descriptors

KwdEn :
- Conceptual analysis, Formal method, Formal specification, Modeling, Refinement method, Reverse engineering, Semantics, Software development, Unified modelling language.

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.

Affiliations:

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

to stream PascalFrancis, to step Corpus: 000361
to stream PascalFrancis, to step Curation: 000664
to stream PascalFrancis, to step Checkpoint: 000294
to stream Main, to step Merge: 004E80
to stream Main, to step Curation: 004D44

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="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</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>
<wicri:noRegion>équipe ESTAS</wicri:noRegion>
<wicri:noRegion>Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ledru, Yves" sort="Ledru, Yves" uniqKey="Ledru Y" first="Yves" last="Ledru">Yves Ledru</name>
<affiliation wicri:level="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Bert, Didier" sort="Bert, Didier" uniqKey="Bert D" first="Didier" last="Bert">Didier Bert</name>
<affiliation wicri:level="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<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>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000294</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000294</idno>
<idno type="wicri:doubleKey">0752-4072:2007:Idani A:approche:formelle:pour</idno>
<idno type="wicri:Area/Main/Merge">004E80</idno>
<idno type="wicri:Area/Main/Curation">004D44</idno>
<idno type="wicri:Area/Main/Exploration">004D44</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="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</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>
<wicri:noRegion>équipe ESTAS</wicri:noRegion>
<wicri:noRegion>Actuellement en post-doc à l'INRETS (Villeneuve d'Ascq), équipe ESTAS</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Ledru, Yves" sort="Ledru, Yves" uniqKey="Ledru Y" first="Yves" last="Ledru">Yves Ledru</name>
<affiliation wicri:level="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Bert, Didier" sort="Bert, Didier" uniqKey="Bert D" first="Didier" last="Bert">Didier Bert</name>
<affiliation wicri:level="3"><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>
<placeName><region type="region" nuts="2">Auvergne-Rhône-Alpes</region>
<region type="old region" nuts="2">Rhône-Alpes</region>
<settlement type="city">St Martin d'Hères</settlement>
</placeName>
</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="2007">2007</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>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>
</textClass>
</profileDesc>
</teiHeader>
<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>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Auvergne-Rhône-Alpes</li>
<li>Rhône-Alpes</li>
</region>
<settlement><li>St Martin d'Hères</li>
</settlement>
</list>
<tree><country name="France"><region name="Auvergne-Rhône-Alpes"><name sortKey="Idani, Akram" sort="Idani, Akram" uniqKey="Idani A" first="Akram" last="Idani">Akram Idani</name>
</region>
<name sortKey="Bert, Didier" sort="Bert, Didier" uniqKey="Bert D" first="Didier" last="Bert">Didier Bert</name>
<name sortKey="Idani, Akram" sort="Idani, Akram" uniqKey="Idani A" first="Akram" last="Idani">Akram Idani</name>
<name sortKey="Ledru, Yves" sort="Ledru, Yves" uniqKey="Ledru Y" first="Yves" last="Ledru">Yves Ledru</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004D44 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004D44 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |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

	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

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

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

Source :

Descripteurs français

English descriptors

Abstract

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

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri