From Requirements to Formal Specification Using UML and B
Identifieur interne : 009061 ( Main/Merge ); précédent : 009060; suivant : 009062From Requirements to Formal Specification Using UML and B
Auteurs : Nicole Lévy [France] ; Rafael Marcano Kamenoff [France] ; Jeanine Souquières [France]Source :
English descriptors
- mix :
Abstract
It is essential to write requirements for every system. They specify what the system is to do, and they are not supposed to say how the system is to achieve those results - that is the responsibility of the design. Requirements must be readable by the different stakeholders. But in addition, they must define exactly and completely the system behaviour. Therefore, they must be consistent. To ensure this last property, the only solution is to use formal methods. But formal notations are recognized as being unreadable and difficult to apply by the customer. We propose a method for the elicitation of requirements and the expression of formal specifications. The approach, expressed in a five-step process, does not introduce a new language but builds on known techniques: the UML semi-formal technique and the B formal technique. It gives methodological support for requirements elicitation and specification development, including the definition of the system tests. The approach is developed on a vending machine case study.
Url:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 002469
- to stream Hal, to step Curation: 002469
- to stream Hal, to step Checkpoint: 005987
Links to Exploration step
Hal:inria-00100758Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">From Requirements to Formal Specification Using UML and B</title><author><name sortKey="Levy, Nicole" sort="Levy, Nicole" uniqKey="Levy N" first="Nicole" last="Lévy">Nicole Lévy</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-31978" status="VALID"><idno type="IdRef">183458028</idno><idno type="RNSR">200312800E</idno><orgName>Parallélisme, Réseaux, Systèmes, Modélisation</orgName><orgName type="acronym">PRISM</orgName><date type="start">2003</date><desc><address><addrLine>UFR des sciences PRISM Bâtiment Descartes 45 avenue des Etats-Unis78035 VERSAILLES</addrLine><country key="FR"></country></address><ref type="url">http://www.prism.uvsq.fr/</ref></desc><listRelation><relation name="FRE3709" active="#struct-81173" type="direct"></relation><relation name="UMR8144" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle name="FRE3709" active="#struct-81173" type="direct"><org type="institution" xml:id="struct-81173" status="VALID"><idno type="IdRef">03082057X</idno><idno type="ISNI">0000 0001 2323 0229 </idno><orgName>Université de Versailles Saint-Quentin-en-Yvelines</orgName><orgName type="acronym">UVSQ</orgName><date type="start">1991-07-22</date><desc><address><addrLine>55 avenue de Paris - 78035 Versailles cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.uvsq.fr/</ref></desc></org></tutelle><tutelle name="UMR8144" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Versailles</settlement><region type="region" nuts="2">Île-de-France</region></placeName><orgName type="university">Université de Versailles-Saint-Quentin-en-Yvelines</orgName></affiliation></author><author><name sortKey="Marcano Kamenoff, Rafael" sort="Marcano Kamenoff, Rafael" uniqKey="Marcano Kamenoff R" first="Rafael" last="Marcano Kamenoff">Rafael Marcano Kamenoff</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-31978" status="VALID"><idno type="IdRef">183458028</idno><idno type="RNSR">200312800E</idno><orgName>Parallélisme, Réseaux, Systèmes, Modélisation</orgName><orgName type="acronym">PRISM</orgName><date type="start">2003</date><desc><address><addrLine>UFR des sciences PRISM Bâtiment Descartes 45 avenue des Etats-Unis78035 VERSAILLES</addrLine><country key="FR"></country></address><ref type="url">http://www.prism.uvsq.fr/</ref></desc><listRelation><relation name="FRE3709" active="#struct-81173" type="direct"></relation><relation name="UMR8144" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle name="FRE3709" active="#struct-81173" type="direct"><org type="institution" xml:id="struct-81173" status="VALID"><idno type="IdRef">03082057X</idno><idno type="ISNI">0000 0001 2323 0229 </idno><orgName>Université de Versailles Saint-Quentin-en-Yvelines</orgName><orgName type="acronym">UVSQ</orgName><date type="start">1991-07-22</date><desc><address><addrLine>55 avenue de Paris - 78035 Versailles cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.uvsq.fr/</ref></desc></org></tutelle><tutelle name="UMR8144" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Versailles</settlement><region type="region" nuts="2">Île-de-France</region></placeName><orgName type="university">Université de Versailles-Saint-Quentin-en-Yvelines</orgName></affiliation></author><author><name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquières">Jeanine Souquières</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2492" status="OLD"><orgName>Development of specifications</orgName><orgName type="acronym">DEDALE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/dedale</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:inria-00100758</idno><idno type="halId">inria-00100758</idno><idno type="halUri">https://hal.inria.fr/inria-00100758</idno><idno type="url">https://hal.inria.fr/inria-00100758</idno><date when="2002">2002</date><idno type="wicri:Area/Hal/Corpus">002469</idno><idno type="wicri:Area/Hal/Curation">002469</idno><idno type="wicri:Area/Hal/Checkpoint">005987</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">005987</idno><idno type="wicri:Area/Main/Merge">009061</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">From Requirements to Formal Specification Using UML and B</title><author><name sortKey="Levy, Nicole" sort="Levy, Nicole" uniqKey="Levy N" first="Nicole" last="Lévy">Nicole Lévy</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-31978" status="VALID"><idno type="IdRef">183458028</idno><idno type="RNSR">200312800E</idno><orgName>Parallélisme, Réseaux, Systèmes, Modélisation</orgName><orgName type="acronym">PRISM</orgName><date type="start">2003</date><desc><address><addrLine>UFR des sciences PRISM Bâtiment Descartes 45 avenue des Etats-Unis78035 VERSAILLES</addrLine><country key="FR"></country></address><ref type="url">http://www.prism.uvsq.fr/</ref></desc><listRelation><relation name="FRE3709" active="#struct-81173" type="direct"></relation><relation name="UMR8144" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle name="FRE3709" active="#struct-81173" type="direct"><org type="institution" xml:id="struct-81173" status="VALID"><idno type="IdRef">03082057X</idno><idno type="ISNI">0000 0001 2323 0229 </idno><orgName>Université de Versailles Saint-Quentin-en-Yvelines</orgName><orgName type="acronym">UVSQ</orgName><date type="start">1991-07-22</date><desc><address><addrLine>55 avenue de Paris - 78035 Versailles cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.uvsq.fr/</ref></desc></org></tutelle><tutelle name="UMR8144" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Versailles</settlement><region type="region" nuts="2">Île-de-France</region></placeName><orgName type="university">Université de Versailles-Saint-Quentin-en-Yvelines</orgName></affiliation></author><author><name sortKey="Marcano Kamenoff, Rafael" sort="Marcano Kamenoff, Rafael" uniqKey="Marcano Kamenoff R" first="Rafael" last="Marcano Kamenoff">Rafael Marcano Kamenoff</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-31978" status="VALID"><idno type="IdRef">183458028</idno><idno type="RNSR">200312800E</idno><orgName>Parallélisme, Réseaux, Systèmes, Modélisation</orgName><orgName type="acronym">PRISM</orgName><date type="start">2003</date><desc><address><addrLine>UFR des sciences PRISM Bâtiment Descartes 45 avenue des Etats-Unis78035 VERSAILLES</addrLine><country key="FR"></country></address><ref type="url">http://www.prism.uvsq.fr/</ref></desc><listRelation><relation name="FRE3709" active="#struct-81173" type="direct"></relation><relation name="UMR8144" active="#struct-441569" type="direct"></relation></listRelation><tutelles><tutelle name="FRE3709" active="#struct-81173" type="direct"><org type="institution" xml:id="struct-81173" status="VALID"><idno type="IdRef">03082057X</idno><idno type="ISNI">0000 0001 2323 0229 </idno><orgName>Université de Versailles Saint-Quentin-en-Yvelines</orgName><orgName type="acronym">UVSQ</orgName><date type="start">1991-07-22</date><desc><address><addrLine>55 avenue de Paris - 78035 Versailles cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.uvsq.fr/</ref></desc></org></tutelle><tutelle name="UMR8144" active="#struct-441569" type="direct"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Versailles</settlement><region type="region" nuts="2">Île-de-France</region></placeName><orgName type="university">Université de Versailles-Saint-Quentin-en-Yvelines</orgName></affiliation></author><author><name sortKey="Souquieres, Jeanine" sort="Souquieres, Jeanine" uniqKey="Souquieres J" first="Jeanine" last="Souquières">Jeanine Souquières</name><affiliation wicri:level="1"><hal:affiliation type="researchteam" xml:id="struct-2492" status="OLD"><orgName>Development of specifications</orgName><orgName type="acronym">DEDALE</orgName><desc><address><country key="FR"></country></address><ref type="url">http://www.loria.fr/la-recherche-en/equipes/dedale</ref></desc><listRelation><relation active="#struct-160" type="direct"></relation><relation name="UMR7503" active="#struct-441569" type="indirect"></relation><relation active="#struct-300009" type="indirect"></relation><relation active="#struct-300291" type="indirect"></relation><relation active="#struct-300292" type="indirect"></relation><relation active="#struct-300293" type="indirect"></relation></listRelation><tutelles><tutelle active="#struct-160" type="direct"><org type="laboratory" xml:id="struct-160" status="OLD"><orgName>Laboratoire Lorrain de Recherche en Informatique et ses Applications</orgName><orgName type="acronym">LORIA</orgName><desc><address><addrLine>Campus Scientifique BP 239 54506 Vandoeuvre-lès-Nancy Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.loria.fr</ref></desc><listRelation><relation name="UMR7503" active="#struct-441569" type="direct"></relation><relation active="#struct-300009" type="direct"></relation><relation active="#struct-300291" type="direct"></relation><relation active="#struct-300292" type="direct"></relation><relation active="#struct-300293" type="direct"></relation></listRelation></org></tutelle><tutelle name="UMR7503" active="#struct-441569" type="indirect"><org type="institution" xml:id="struct-441569" status="VALID"><idno type="ISNI">0000000122597504</idno><idno type="IdRef">02636817X</idno><orgName>Centre National de la Recherche Scientifique</orgName><orgName type="acronym">CNRS</orgName><date type="start">1939-10-19</date><desc><address><country key="FR"></country></address><ref type="url">http://www.cnrs.fr/</ref></desc></org></tutelle><tutelle active="#struct-300009" type="indirect"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle><tutelle active="#struct-300291" type="indirect"><org type="institution" xml:id="struct-300291" status="OLD"><orgName>Université Henri Poincaré - Nancy 1</orgName><orgName type="acronym">UHP</orgName><date type="end">2011-12-31</date><desc><address><addrLine>24-30 rue Lionnois, BP 60120, 54 003 NANCY cedex, France</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300292" type="indirect"><org type="institution" xml:id="struct-300292" status="OLD"><orgName>Université Nancy 2</orgName><date type="end">2011-12-31</date><desc><address><addrLine>91 avenue de la Libération, BP 454, 54001 Nancy cedex</addrLine><country key="FR"></country></address></desc></org></tutelle><tutelle active="#struct-300293" type="indirect"><org type="institution" xml:id="struct-300293" status="OLD"><orgName>Institut National Polytechnique de Lorraine</orgName><orgName type="acronym">INPL</orgName><date type="end">2011-12-31</date><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Université Nancy 2</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName><placeName><settlement type="city">Nancy</settlement><region type="region" nuts="2">Grand Est</region><region type="old region" nuts="2">Lorraine (région)</region></placeName><orgName type="university">Institut national polytechnique de Lorraine</orgName><orgName type="institution" wicri:auto="newGroup">Université de Lorraine</orgName></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term>b</term><term>formal specification</term><term>requirements</term><term>uml</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">It is essential to write requirements for every system. They specify what the system is to do, and they are not supposed to say how the system is to achieve those results - that is the responsibility of the design. Requirements must be readable by the different stakeholders. But in addition, they must define exactly and completely the system behaviour. Therefore, they must be consistent. To ensure this last property, the only solution is to use formal methods. But formal notations are recognized as being unreadable and difficult to apply by the customer. We propose a method for the elicitation of requirements and the expression of formal specifications. The approach, expressed in a five-step process, does not introduce a new language but builds on known techniques: the UML semi-formal technique and the B formal technique. It gives methodological support for requirements elicitation and specification development, including the definition of the system tests. The approach is developed on a vending machine case study.</div></front></TEI></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 009061 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 009061 | 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é= Hal:inria-00100758
|texte= From Requirements to Formal Specification Using UML and B
}}
| This area was generated with Dilib version V0.6.33. |  |