Consistency in UML and B multi-view specifications
Identifieur interne : 004183 ( Crin/Corpus ); précédent : 004182; suivant : 004184Consistency in UML and B multi-view specifications
Auteurs : Dieu Donné Okalas Ossami ; Jeanine Souquières ; Jean-Pierre JacquotSource :
English descriptors
- KwdEn :
- b , consistency, multi-view, operator, uml, verification.
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.
Links to Exploration step
CRIN:okalas_ossami05aLe document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" wicri:score="301">Consistency in UML and B multi-view specifications</title></titleStmt><publicationStmt><idno type="RBID">CRIN:okalas_ossami05a</idno><date when="2005" year="2005">2005</date><idno type="wicri:Area/Crin/Corpus">004183</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">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></author><author><name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquières">Jeanine Souquières</name></author><author><name sortKey="Jacquot, Jean Pierre" sort="Jacquot, Jean Pierre" uniqKey="Jacquot J" first="Jean-Pierre" last="Jacquot">Jean-Pierre Jacquot</name></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>b
</term><term>consistency</term><term>multi-view</term><term>operator</term><term>uml</term><term>verification</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en" wicri:score="2111">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></TEI><BibTex type="inproceedings"><ref>okalas_ossami05a</ref><crinnumber>A05-R-181</crinnumber><category>3</category><equipe>DEDALE</equipe><author><e>Okalas Ossami, Dieu Donné</e><e>Souquières, Jeanine</e><e>Jacquot, Jean-Pierre</e></author><title>Consistency in UML and B multi-view specifications</title><booktitle>{Fifth International Conference on Integrated Formal Methods - IFM'2005, Eindhoven, The Netherlands }</booktitle><year>2005</year><month>Nov</month><publisher>Springer</publisher><keywords><e>consistency</e><e>verification</e><e>operator</e><e>multi-view</e><e>uml</e><e>b
</e></keywords><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.</abstract></BibTex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Crin/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004183 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Crin/Corpus/biblio.hfd -nk 004183 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Crin
|étape= Corpus
|type= RBID
|clé= CRIN:okalas_ossami05a
|texte= Consistency in UML and B multi-view specifications
}}
| This area was generated with Dilib version V0.6.33. |  |