Consistency in UML and B multi-view specifications
Identifieur interne :
000553 ( PascalFrancis/Curation );
précédent :
000552;
suivant :
000554
Consistency in UML and B multi-view specifications
Auteurs : Dieu Donné Okalas Ossami [
France] ;
Jean-Pierre Jacquot [
France] ;
Jeanine Souquieres [
France]
Source :
-
Lecture notes in computer science [ 0302-9743 ] ; 2005.
RBID : Pascal:06-0070353
Descripteurs français
English descriptors
Abstract
We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.
| pA |
| A01 | 01 | 1 | | @0 0302-9743 |
|---|
| A05 | | | | @2 3771 |
|---|
| A08 | 01 | 1 | ENG | @1 Consistency in UML and B multi-view specifications |
|---|
| A09 | 01 | 1 | ENG | @1 Integrated formal methods : 5th international conference, IFM 2005 : Eindhoven, The Netherlands, November 29-December 2, 2005 : proceedings |
|---|
| A11 | 01 | 1 | | @1 OKALAS OSSAMI (Dieu Donné) |
|---|
| A11 | 02 | 1 | | @1 JACQUOT (Jean-Pierre) |
|---|
| A11 | 03 | 1 | | @1 SOUQUIERES (Jeanine) |
|---|
| A14 | 01 | | | @1 LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut. @Z 3 aut. |
|---|
| A20 | | | | @1 386-405 |
|---|
| A21 | | | | @1 2005 |
|---|
| A23 | 01 | | | @0 ENG |
|---|
| A26 | 01 | | | @0 3-540-30492-4 |
|---|
| A43 | 01 | | | @1 INIST @2 16343 @5 354000138673130220 |
|---|
| A44 | | | | @0 0000 @1 © 2006 INIST-CNRS. All rights reserved. |
|---|
| A45 | | | | @0 27 ref. |
|---|
| A47 | 01 | 1 | | @0 06-0070353 |
|---|
| A60 | | | | @1 P @2 C |
|---|
| A61 | | | | @0 A |
|---|
| A64 | 01 | 1 | | @0 Lecture notes in computer science |
|---|
| A66 | 01 | | | @0 DEU |
|---|
| C01 | 01 | | ENG | @0 We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model. |
|---|
| C02 | 01 | X | | @0 001D02B09 |
|---|
| C03 | 01 | X | FRE | @0 Méthode formelle @5 01 |
|---|
| C03 | 01 | X | ENG | @0 Formal method @5 01 |
|---|
| C03 | 01 | X | SPA | @0 Método formal @5 01 |
|---|
| C03 | 02 | X | FRE | @0 Vérification programme @5 02 |
|---|
| C03 | 02 | X | ENG | @0 Program verification @5 02 |
|---|
| C03 | 02 | X | SPA | @0 Verificación programa @5 02 |
|---|
| C03 | 03 | X | FRE | @0 Langage modélisation unifié @5 06 |
|---|
| C03 | 03 | X | ENG | @0 Unified modelling language @5 06 |
|---|
| C03 | 03 | X | SPA | @0 Lenguaje UML @5 06 |
|---|
| C03 | 04 | X | FRE | @0 Vue multiple @5 18 |
|---|
| C03 | 04 | X | ENG | @0 Multiple view @5 18 |
|---|
| C03 | 04 | X | SPA | @0 Vista múltiple @5 18 |
|---|
| C03 | 05 | X | FRE | @0 Relation sémantique @5 19 |
|---|
| C03 | 05 | X | ENG | @0 Semantic relation @5 19 |
|---|
| C03 | 05 | X | SPA | @0 Relación semántica @5 19 |
|---|
| C03 | 06 | X | FRE | @0 Modélisation @5 23 |
|---|
| C03 | 06 | X | ENG | @0 Modeling @5 23 |
|---|
| C03 | 06 | X | SPA | @0 Modelización @5 23 |
|---|
| N21 | | | | @1 037 |
|---|
| N44 | 01 | | | @1 OTO |
|---|
| N82 | | | | @1 OTO |
|---|
|
|---|
| pR |
| A30 | 01 | 1 | ENG | @1 Integrated formal methods. International conference @2 5 @3 Eindhoven NLD @4 2005-11-29 |
|---|
|
|---|
Links toward previous steps (curation, corpus...)
- to stream PascalFrancis, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000480
Links to Exploration step
Pascal:06-0070353
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Consistency in UML and B multi-view specifications</title>
<author><name sortKey="Okalas Ossami, Dieu Donne" sort="Okalas Ossami, Dieu Donne" uniqKey="Okalas Ossami D" first="Dieu Donné" last="Okalas Ossami">Dieu Donné Okalas Ossami</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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="Jacquot, Jean Pierre" sort="Jacquot, Jean Pierre" uniqKey="Jacquot J" first="Jean-Pierre" last="Jacquot">Jean-Pierre Jacquot</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquieres">Jeanine Souquieres</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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">06-0070353</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 06-0070353 INIST</idno>
<idno type="RBID">Pascal:06-0070353</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000480</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000553</idno>
</publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Consistency in UML and B multi-view specifications</title>
<author><name sortKey="Okalas Ossami, Dieu Donne" sort="Okalas Ossami, Dieu Donne" uniqKey="Okalas Ossami D" first="Dieu Donné" last="Okalas Ossami">Dieu Donné Okalas Ossami</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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="Jacquot, Jean Pierre" sort="Jacquot, Jean Pierre" uniqKey="Jacquot J" first="Jean-Pierre" last="Jacquot">Jean-Pierre Jacquot</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquieres">Jeanine Souquieres</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</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">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="2005">2005</date>
</imprint><seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Formal method</term>
<term>Modeling</term>
<term>Multiple view</term>
<term>Program verification</term>
<term>Semantic relation</term>
<term>Unified modelling language</term>
</keywords><keywords scheme="Pascal" xml:lang="fr"><term>Méthode formelle</term>
<term>Vérification programme</term>
<term>Langage modélisation unifié</term>
<term>Vue multiple</term>
<term>Relation sémantique</term>
<term>Modélisation</term>
</keywords><front><div type="abstract" xml:lang="en">We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.</div>
</front><inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01><fA05><s2>3771</s2>
</fA05><fA08 i1="01" i2="1" l="ENG"><s1>Consistency in UML and B multi-view specifications</s1>
</fA08><fA09 i1="01" i2="1" l="ENG"><s1>Integrated formal methods : 5th international conference, IFM 2005 : Eindhoven, The Netherlands, November 29-December 2, 2005 : proceedings</s1>
</fA09><fA11 i1="01" i2="1"><s1>OKALAS OSSAMI (Dieu Donné)</s1>
</fA11><fA11 i1="02" i2="1"><s1>JACQUOT (Jean-Pierre)</s1>
</fA11><fA11 i1="03" i2="1"><s1>SOUQUIERES (Jeanine)</s1>
</fA11><fA14 i1="01"><s1>LORIA, University Nancy 2, UHP Nancy 1, Campus scientifique, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
<sZ>3 aut.</sZ>
</fA14><fA20><s1>386-405</s1>
</fA20><fA21><s1>2005</s1>
</fA21><fA23 i1="01"><s0>ENG</s0>
</fA23><fA26 i1="01"><s0>3-540-30492-4</s0>
</fA26><fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000138673130220</s5>
</fA43><fA44><s0>0000</s0>
<s1>© 2006 INIST-CNRS. All rights reserved.</s1>
</fA44><fA45><s0>27 ref.</s0>
</fA45><fA47 i1="01" i2="1"><s0>06-0070353</s0>
</fA47><fA60><s1>P</s1>
<s2>C</s2>
</fA60><fA64 i1="01" i2="1"><s0>Lecture notes in computer science</s0>
</fA64><fA66 i1="01"><s0>DEU</s0>
</fA66><fC01 i1="01" l="ENG"><s0>We present the notion of consistency relation in UML and B multi-view specifications. It is defined as a semantic relation between both views. It provides us with a sound basis to define the notion of development operator. An operator models a development step; it separates the design decisions from their expression in the specification formalisms. Operator correctness is defined as a property which guarantees that the application of an operator on a consistent specification state yields a consistent new state. An operator can be proven once and for all to be correct. A classical case-study, the Generalized Railroad Crossing (GRC), demonstrates how the different notions can be put in practice to provide specifiers with a realistic development model.</s0>
</fC01><fC02 i1="01" i2="X"><s0>001D02B09</s0>
</fC02><fC03 i1="01" i2="X" l="FRE"><s0>Méthode formelle</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="ENG"><s0>Formal method</s0>
<s5>01</s5>
</fC03><fC03 i1="01" i2="X" l="SPA"><s0>Método formal</s0>
<s5>01</s5>
</fC03><fC03 i1="02" i2="X" l="FRE"><s0>Vérification programme</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="ENG"><s0>Program verification</s0>
<s5>02</s5>
</fC03><fC03 i1="02" i2="X" l="SPA"><s0>Verificación programa</s0>
<s5>02</s5>
</fC03><fC03 i1="03" i2="X" l="FRE"><s0>Langage modélisation unifié</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="ENG"><s0>Unified modelling language</s0>
<s5>06</s5>
</fC03><fC03 i1="03" i2="X" l="SPA"><s0>Lenguaje UML</s0>
<s5>06</s5>
</fC03><fC03 i1="04" i2="X" l="FRE"><s0>Vue multiple</s0>
<s5>18</s5>
</fC03><fC03 i1="04" i2="X" l="ENG"><s0>Multiple view</s0>
<s5>18</s5>
</fC03><fC03 i1="04" i2="X" l="SPA"><s0>Vista múltiple</s0>
<s5>18</s5>
</fC03><fC03 i1="05" i2="X" l="FRE"><s0>Relation sémantique</s0>
<s5>19</s5>
</fC03><fC03 i1="05" i2="X" l="ENG"><s0>Semantic relation</s0>
<s5>19</s5>
</fC03><fC03 i1="05" i2="X" l="SPA"><s0>Relación semántica</s0>
<s5>19</s5>
</fC03><fC03 i1="06" i2="X" l="FRE"><s0>Modélisation</s0>
<s5>23</s5>
</fC03><fC03 i1="06" i2="X" l="ENG"><s0>Modeling</s0>
<s5>23</s5>
</fC03><fC03 i1="06" i2="X" l="SPA"><s0>Modelización</s0>
<s5>23</s5>
</fC03><fN21><s1>037</s1>
</fN21><fN44 i1="01"><s1>OTO</s1>
</fN44><fN82><s1>OTO</s1>
</fN82><pR><fA30 i1="01" i2="1" l="ENG"><s1>Integrated formal methods. International conference</s1>
<s2>5</s2>
<s3>Eindhoven NLD</s3>
<s4>2005-11-29</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 000553 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Curation/biblio.hfd -nk 000553 | 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:06-0070353
|texte= Consistency in UML and B multi-view specifications
}}
| 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 |  |
