B : passé, présent, futur
Identifieur interne : 007D34 ( Main/Merge ); précédent : 007D33; suivant : 007D35B : passé, présent, futur
Auteurs : Jean-Raymond Abrial [France]Source :
- Technique et Science Informatiques [ 0752-4072 ] ; 2003.
Abstract
Cet article est une présentation non technique, mais rigoureuse, de la méthode B. Il s'adresse aux lecteurs qui ont entendu parler de B et qui souhaitent en savoir davantage. Il indique quelle est la démarche initiale de B et sa raison d'être, c'est-à-dire la modélisation de logiciels et plus généralement des systèmes. Il précise ensuite ce qu'est un modèle et décrit les concepts importants de la méthode, à savoir le raffinement, la décomposition et la généricité. La méthode B permet d'envisager les modèles sous deux aspects : la vision locale et la vision globale. Le deuxième aspect utilise une nouvelle façon d'écrire le B, appelée “B-événementiel”. La correction des logiciels produits par la méthode B est assurée par des preuves mathématiques. L'article explique ce que signifie “prouver” et quand ces preuves doivent être faites. Enfin, il indique comment intégrer B dans le contexte industriel pour la construction de systèmes opérationnels. L'article est illustré par quelques exemples informels, tirés da la pratique de B.
This paper is a non technical, yet rigorous, presentation of the B method. It is intended to be read by people who know a little about B and want to know more. It first presents the main approach of B, its raison d'être, namely the construction of models of software and more generally of discrete systems. It then makes precise what is meant by a "model", and also describes the important concepts at work in this approach, namely those of refinement, decomposition, and genericity. In applying B, two broad kinds of models are envisaged: those devoted to a "local" vision and those devoted to a "global" one. The second vision uses a new approach in writing B models, which is called "Event B". The correctness of programs written thanks to B are enforced by using formal proofs. It is explained what it means to "prove" a model and also how such proofs can be performed in practice. Finally, the paper shows how such an approach can be incorporated within an industrial environment in order to build operational systems. A number of practical examples illustrates the various facets presented in the paper.
Url:
DOI: 10.3166/tsi.22.00-89
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003967
- to stream Istex, to step Curation: 003923
- to stream Istex, to step Checkpoint: 001945
Links to Exploration step
ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FEDLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="fr">B : passé, présent, futur</title><author><name sortKey="Abrial, Jean Raymond" sort="Abrial, Jean Raymond" uniqKey="Abrial J" first="Jean-Raymond" last="Abrial">Jean-Raymond Abrial</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FED</idno><date when="2003" year="2003">2003</date><idno type="doi">10.3166/tsi.22.00-89</idno><idno type="url">https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003967</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003967</idno><idno type="wicri:Area/Istex/Curation">003923</idno><idno type="wicri:Area/Istex/Checkpoint">001945</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001945</idno><idno type="wicri:doubleKey">0752-4072:2003:Abrial J:b:passe:present</idno><idno type="wicri:Area/Main/Merge">007D34</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="fr">B : passé, présent, futur</title><author><name sortKey="Abrial, Jean Raymond" sort="Abrial, Jean Raymond" uniqKey="Abrial J" first="Jean-Raymond" last="Abrial">Jean-Raymond Abrial</name><affiliation wicri:level="1"><country>France</country><placeName><settlement type="city">Marseille</settlement><region type="région" nuts="2">Provence-Alpes-Côte d'Azur</region></placeName><wicri:regionArea>11</wicri:regionArea></affiliation><affiliation><wicri:noCountry code="no comma">E-mail: jr@abrial.org</wicri:noCountry></affiliation></author></analytic><monogr></monogr><series><title level="j" type="main">Technique et Science Informatiques</title><title level="j" type="abbrev">Tech. Sci. Info.</title><idno type="ISSN">0752-4072</idno><idno type="eISSN">2116-5920</idno><imprint><publisher>Lavoisier</publisher><date type="published" when="2003-01">2003</date><biblScope unit="vol">22</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="89">89</biblScope><biblScope unit="page" to="118">118</biblScope><biblScope unit="page-count">30</biblScope><biblScope unit="ref-count">0</biblScope><biblScope unit="fig-count">0</biblScope><biblScope unit="table-count">0</biblScope></imprint><idno type="ISSN">0752-4072</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0752-4072</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="fr">Cet article est une présentation non technique, mais rigoureuse, de la méthode B. Il s'adresse aux lecteurs qui ont entendu parler de B et qui souhaitent en savoir davantage. Il indique quelle est la démarche initiale de B et sa raison d'être, c'est-à-dire la modélisation de logiciels et plus généralement des systèmes. Il précise ensuite ce qu'est un modèle et décrit les concepts importants de la méthode, à savoir le raffinement, la décomposition et la généricité. La méthode B permet d'envisager les modèles sous deux aspects : la vision locale et la vision globale. Le deuxième aspect utilise une nouvelle façon d'écrire le B, appelée “B-événementiel”. La correction des logiciels produits par la méthode B est assurée par des preuves mathématiques. L'article explique ce que signifie “prouver” et quand ces preuves doivent être faites. Enfin, il indique comment intégrer B dans le contexte industriel pour la construction de systèmes opérationnels. L'article est illustré par quelques exemples informels, tirés da la pratique de B.</div><div type="abstract" xml:lang="en">This paper is a non technical, yet rigorous, presentation of the B method. It is intended to be read by people who know a little about B and want to know more. It first presents the main approach of B, its raison d'être, namely the construction of models of software and more generally of discrete systems. It then makes precise what is meant by a "model", and also describes the important concepts at work in this approach, namely those of refinement, decomposition, and genericity. In applying B, two broad kinds of models are envisaged: those devoted to a "local" vision and those devoted to a "global" one. The second vision uses a new approach in writing B models, which is called "Event B". The correctness of programs written thanks to B are enforced by using formal proofs. It is explained what it means to "prove" a model and also how such proofs can be performed in practice. Finally, the paper shows how such an approach can be incorporated within an industrial environment in order to build operational systems. A number of practical examples illustrates the various facets presented in the paper.</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 007D34 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 007D34 | 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é= ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FED
|texte= B : passé, présent, futur
}}
| This area was generated with Dilib version V0.6.33. |  |