InforLorV4, Main, Merge, bibRecord, 005738

Verification of UML model elements using B : Software Engineering and Software

Identifieur interne : 005738 ( Main/Merge ); précédent : 005737; suivant : 005739

Verification of UML model elements using B : Software Engineering and Software

Auteurs : NINH THUAN TRUONG [France] ; Jeanine Souquieres [France]

Source :

Journal of information science and engineering [ 1016-2364 ] ; 2006.

RBID : Pascal:06-0247314

Descripteurs français

Pascal (Inist)
- Métamodèle, Spécification modèle, Vérification formelle, Méthode formelle, Langage formel, Langage modélisation unifié, Spécification formelle, Méthode formelle B.

English descriptors

KwdEn :
- Formal language, Formal method, Formal specification, Formal verification, Metamodel, Model specification, Unified modelling language.

Abstract

We propose an approach to verify UML model elements based on the transformation of the UML meta-model into B formal specifications. The UML meta-model is described as a combination of graphical notations, natural and formal languages. The semantics of UML elements is expressed by well-formedness rules in the UML meta-model. Their correctness is ensured by the proof of the B specifications. The approach is illustrated by a simple case study: the printing system.

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

to stream PascalFrancis, to step Corpus: 000450
to stream PascalFrancis, to step Curation: 000583
to stream PascalFrancis, to step Checkpoint: 000333

Links to Exploration step

Pascal:06-0247314

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Verification of UML model elements using B : Software Engineering and Software</title>
<author><name sortKey="Ninh Thuan Truong" sort="Ninh Thuan Truong" uniqKey="Ninh Thuan Truong" last="Ninh Thuan Truong">NINH THUAN TRUONG</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA - Université Nancy</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquieres">Jeanine Souquieres</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA - Université Nancy</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">06-0247314</idno>
<date when="2006">2006</date>
<idno type="stanalyst">PASCAL 06-0247314 INIST</idno>
<idno type="RBID">Pascal:06-0247314</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000450</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000583</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000333</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000333</idno>
<idno type="wicri:doubleKey">1016-2364:2006:Ninh Thuan Truong:verification:of:uml</idno>
<idno type="wicri:Area/Main/Merge">005738</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Verification of UML model elements using B : Software Engineering and Software</title>
<author><name sortKey="Ninh Thuan Truong" sort="Ninh Thuan Truong" uniqKey="Ninh Thuan Truong" last="Ninh Thuan Truong">NINH THUAN TRUONG</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA - Université Nancy</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
<author><name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquieres">Jeanine Souquieres</name>
<affiliation wicri:level="3"><inist:fA14 i1="01"><s1>LORIA - Université Nancy</s1>
<s2>Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region">Grand Est</region>
<region type="old region">Lorraine (région)</region>
<settlement type="city">Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Journal of information science and engineering</title>
<title level="j" type="abbreviated">J. inf. sci. eng.</title>
<idno type="ISSN">1016-2364</idno>
<imprint><date when="2006">2006</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Journal of information science and engineering</title>
<title level="j" type="abbreviated">J. inf. sci. eng.</title>
<idno type="ISSN">1016-2364</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Formal language</term>
<term>Formal method</term>
<term>Formal specification</term>
<term>Formal verification</term>
<term>Metamodel</term>
<term>Model specification</term>
<term>Unified modelling language</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Métamodèle</term>
<term>Spécification modèle</term>
<term>Vérification formelle</term>
<term>Méthode formelle</term>
<term>Langage formel</term>
<term>Langage modélisation unifié</term>
<term>Spécification formelle</term>
<term>Méthode formelle B</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We propose an approach to verify UML model elements based on the transformation of the UML meta-model into B formal specifications. The UML meta-model is described as a combination of graphical notations, natural and formal languages. The semantics of UML elements is expressed by well-formedness rules in the UML meta-model. Their correctness is ensured by the proof of the B specifications. The approach is illustrated by a simple case study: the printing system.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Nancy</li>
</settlement>
</list>
<tree><country name="France"><region name="Grand Est"><name sortKey="Ninh Thuan Truong" sort="Ninh Thuan Truong" uniqKey="Ninh Thuan Truong" last="Ninh Thuan Truong">NINH THUAN TRUONG</name>
</region>
<name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquieres">Jeanine Souquieres</name>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

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

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

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 005738 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Merge
   |type=    RBID
   |clé=     Pascal:06-0247314
   |texte=   Verification of UML model elements using B : Software Engineering and Software
}}

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

Verification of UML model elements using B : Software Engineering and Software

Verification of UML model elements using B : Software Engineering and Software

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