InforLorV4, Istex, Corpus, bibRecord, 003967

B : passé, présent, futur

Identifieur interne : 003967 ( Istex/Corpus ); précédent : 003966; suivant : 003968

B : passé, présent, futur

Source :

Technique et Science Informatiques [ 0752-4072 ] ; 2003.

RBID : ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FED

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:

https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/fulltext.pdf

DOI: 10.3166/tsi.22.00-89

Links to Exploration step

ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FED

Le 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>
<affiliation><mods:affiliation>11, rue Chateauredon F-13001 Marseille</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: jr@abrial.org</mods:affiliation>
</affiliation>
</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>
</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><mods:affiliation>11, rue Chateauredon F-13001 Marseille</mods:affiliation>
</affiliation>
<affiliation><mods:affiliation>E-mail: jr@abrial.org</mods:affiliation>
</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>
<istex><corpusName>lavoisier</corpusName>
<author><json:item><name>Jean-Raymond Abrial</name>
<affiliations><json:string>11, rue Chateauredon F-13001 Marseille</json:string>
<json:string>E-mail: jr@abrial.org</json:string>
</affiliations>
</json:item>
</author>
<subject><json:item><lang><json:string>fre</json:string>
</lang>
<value>Modélisation</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>construction de logiciels et de systèmes</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>vérification de propriétés</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>méthode B</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>Modelisation</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>software and system construction</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>property verification</value>
</json:item>
<json:item><lang><json:string>fre</json:string>
</lang>
<value>B method</value>
</json:item>
</subject>
<arkIstex>ark:/67375/HT0-FLG759KZ-Q</arkIstex>
<language><json:string>fre</json:string>
</language>
<originalGenre><json:string>research-article</json:string>
</originalGenre>
<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.</abstract>
<qualityIndicators><score>8.956</score>
<pdfWordCount>12718</pdfWordCount>
<pdfCharCount>74065</pdfCharCount>
<pdfVersion>1.3</pdfVersion>
<pdfPageCount>30</pdfPageCount>
<pdfPageSize>595 x 842 pts (A4)</pdfPageSize>
<refBibsNative>false</refBibsNative>
<abstractWordCount>163</abstractWordCount>
<abstractCharCount>1038</abstractCharCount>
<keywordCount>8</keywordCount>
</qualityIndicators>
<title>B : passé, présent, futur</title>
<genre><json:string>research-article</json:string>
</genre>
<host><title>Technique et Science Informatiques</title>
<language><json:string>unknown</json:string>
</language>
<issn><json:string>0752-4072</json:string>
</issn>
<eissn><json:string>2116-5920</json:string>
</eissn>
<publisherId><json:string>tsi</json:string>
</publisherId>
<volume>22</volume>
<issue>1</issue>
<pages><first>89</first>
<last>118</last>
<total>30</total>
</pages>
<genre><json:string>journal</json:string>
</genre>
<subject><json:item><value>SYNTHÈSE</value>
</json:item>
</subject>
</host>
<ark><json:string>ark:/67375/HT0-FLG759KZ-Q</json:string>
</ark>
<publicationDate>2003</publicationDate>
<copyrightDate>2003</copyrightDate>
<doi><json:string>10.3166/tsi.22.00-89</json:string>
</doi>
<id>F0A66F68D05118BF8CCC53FBABD6958272344FED</id>
<score>1</score>
<fulltext><json:item><extension>pdf</extension>
<original>true</original>
<mimetype>application/pdf</mimetype>
<uri>https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/fulltext.pdf</uri>
</json:item>
<json:item><extension>zip</extension>
<original>false</original>
<mimetype>application/zip</mimetype>
<uri>https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/bundle.zip</uri>
</json:item>
<istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main">B : passé, présent, futur</title>
<respStmt><resp>Références bibliographiques récupérées via GROBID</resp>
<name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name>
</respStmt>
</titleStmt>
<publicationStmt><authority>ISTEX</authority>
<publisher>Lavoisier</publisher>
<availability><licence>© Lavoisier SAS 2003</licence>
<p>Lavoisier SAS</p>
</availability>
<date type="published" when="2003-01">2003</date>
<date type="Copyright" when="2003">2003</date>
</publicationStmt>
<notesStmt><note type="content-type" source="research-article" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</note>
<note type="publication-type" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</note>
</notesStmt>
<sourceDesc><biblStruct type="article"><analytic><title level="a" type="main" xml:lang="fr">B : passé, présent, futur</title>
<author xml:id="author-0000" role="corresp"><persName><surname>Abrial</surname>
<forename type="first">Jean-Raymond</forename>
</persName>
<affiliation><ref>1</ref>
<address><street>11, rue Chateauredon</street>
<postCode>F-13001</postCode>
<settlement>Marseille</settlement>
</address>
</affiliation>
<email>jr@abrial.org</email>
</author>
<idno type="istex">F0A66F68D05118BF8CCC53FBABD6958272344FED</idno>
<idno type="ark">ark:/67375/HT0-FLG759KZ-Q</idno>
<idno type="DOI">10.3166/tsi.22.00-89</idno>
<idno type="publisher-id">tsi221p118</idno>
</analytic>
<monogr><title level="j" type="main">Technique et Science Informatiques</title>
<title level="j" type="abbrev">Tech. Sci. Info.</title>
<idno type="publisher-id">tsi</idno>
<idno type="pISSN">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>
</monogr>
</biblStruct>
</sourceDesc>
</fileDesc>
<profileDesc><abstract xml:lang="fr"><p>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.</p>
</abstract>
<abstract xml:lang="en"><p>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.</p>
</abstract>
<textClass ana="subject"><keywords scheme="section"><term>SYNTHÈSE</term>
</keywords>
</textClass>
<textClass ana="keyword"><keywords xml:lang="fr"><term>Modélisation</term>
<term>construction de logiciels et de systèmes</term>
<term>vérification de propriétés</term>
<term>méthode B</term>
</keywords>
</textClass>
<textClass ana="keyword"><keywords xml:lang="en"><term>Modelisation</term>
<term>software and system construction</term>
<term>property verification</term>
<term>B method</term>
</keywords>
</textClass>
<langUsage><language ident="fr"></language>
</langUsage>
</profileDesc>
<revisionDesc><change xml:id="refBibs-istex" who="#ISTEX-API" when="2019-01-15">References added</change>
</revisionDesc>
</teiHeader>
</istex:fulltextTEI>
<json:item><extension>txt</extension>
<original>false</original>
<mimetype>text/plain</mimetype>
<uri>https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/fulltext.txt</uri>
</json:item>
</fulltext>
<metadata><istex:metadataXml wicri:clean="corpus lavoisier not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration>
<istex:docType PUBLIC="-//EDP//DTD EDP Publishing JATS v1.0 20130606//EN" URI="JATS-edppublishing1.dtd" name="istex:docType"></istex:docType>
<istex:document><article article-type="research-article" dtd-version="1.0" xml:lang="fr">

  <front>

		<journal-meta>

			<journal-id journal-id-type="publisher-id">tsi</journal-id>

			<journal-title-group>

				<journal-title>Technique et Science Informatiques</journal-title>

				<abbrev-journal-title abbrev-type="publisher">Tech. Sci. Info.</abbrev-journal-title>

			</journal-title-group>

			<issn pub-type="ppub">0752-4072</issn>

			<issn pub-type="epub">2116-5920</issn>

			<publisher>

				<publisher-name>Lavoisier</publisher-name>

			</publisher>

		</journal-meta>

    <article-meta>

      <article-id pub-id-type="doi">10.3166/tsi.22.00-89</article-id>

      <article-id pub-id-type="publisher-id">tsi221p118</article-id>

<article-categories>

				<subj-group subj-group-type="section" xml:lang="fr">

					<subject>SYNTHÈSE</subject>

				</subj-group>

</article-categories>

      <title-group>

        <article-title xml:lang="fr">B : passé, présent, futur</article-title>

      </title-group>

      <contrib-group content-type="authors">

        <contrib contrib-type="author" corresp="yes">

          <name>

            <surname>Abrial</surname>

            <given-names>Jean-Raymond</given-names>

          </name>

          <xref ref-type="aff" rid="AFF1">1</xref>

          <xref ref-type="corresp" rid="FN1">*</xref>

        </contrib>

      </contrib-group>

      <aff id="AFF1"><label>1</label>
<addr-line><named-content content-type="street">11, rue Chateauredon</named-content>
 <named-content content-type="postcode">F-13001</named-content>
 <named-content content-type="city">Marseille</named-content>
</addr-line>
 </aff>

      <author-notes>

        <corresp id="FN1">

          <label>*</label>

          <email>jr@abrial.org</email>

        </corresp>

      </author-notes>

			<pub-date date-type="pub" publication-format="print">

				<month>01</month>

				<year>2003</year>

			</pub-date>

			<volume>22</volume>

			<issue>1</issue>

			<fpage>89</fpage>

			<lpage>118</lpage>

      <permissions>

				<copyright-statement>© Lavoisier SAS 2003</copyright-statement>

				<copyright-year>2003</copyright-year>

				<copyright-holder>Lavoisier SAS</copyright-holder>

      </permissions>

      <abstract xml:lang="fr">

        <p>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.</p>

      </abstract>

      <trans-abstract xml:lang="en">

        <p>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.</p>

      </trans-abstract>

      <kwd-group xml:lang="fr">

        <kwd>Modélisation</kwd>

        <kwd>construction de logiciels et de systèmes</kwd>

        <kwd>vérification de propriétés</kwd>

        <kwd>méthode B</kwd>

      </kwd-group>

      <kwd-group xml:lang="en">

        <kwd>Modelisation</kwd>

        <kwd>software and system construction</kwd>

        <kwd>property verification</kwd>

        <kwd>B method</kwd>

      </kwd-group>

      <counts>

        <fig-count count="0"></fig-count>

        <table-count count="0"></table-count>

        <equation-count count="0"></equation-count>

        <ref-count count="0"></ref-count>

        <page-count count="30"></page-count>

      </counts>

      <custom-meta-group>

        <custom-meta>

					<meta-name>idline</meta-name>

					<meta-value>TSI. Volume 22

					– n° 1/2003,

					pages 89 à 118</meta-value>

        </custom-meta>

        <custom-meta>

					<meta-name>cover_date</meta-name>

					<meta-value>Janvier 2003</meta-value>

        </custom-meta>

        <custom-meta>

					<meta-name>first_month</meta-name>

					<meta-value>01</meta-value>

        </custom-meta>

        <custom-meta>

					<meta-name>last_month</meta-name>

					<meta-value>01</meta-value>

        </custom-meta>

        <custom-meta>

					<meta-name>first_year</meta-name>

					<meta-value>2003</meta-value>

        </custom-meta>

        <custom-meta>

					<meta-name>last_year</meta-name>

					<meta-value>2003</meta-value>

        </custom-meta>

      </custom-meta-group>

    </article-meta>

  </front>

</article>

</istex:document>
</istex:metadataXml>
<mods version="3.6"><titleInfo lang="fr"><title>B : passé, présent, futur</title>
</titleInfo>
<titleInfo type="alternative" lang="fr" contentType="CDATA"><title>B : passé, présent, futur</title>
</titleInfo>
<name type="personal"><namePart type="given">Jean-Raymond</namePart>
<namePart type="family">Abrial</namePart>
<affiliation>11, rue Chateauredon F-13001 Marseille</affiliation>
<affiliation>E-mail: jr@abrial.org</affiliation>
<role><roleTerm type="text">author</roleTerm>
</role>
</name>
<typeOfResource>text</typeOfResource>
<genre type="research-article" displayLabel="research-article" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-1JC4F85T-7">research-article</genre>
<originInfo><publisher>Lavoisier</publisher>
<dateIssued encoding="w3cdtf">2003</dateIssued>
<copyrightDate encoding="w3cdtf">2003</copyrightDate>
</originInfo>
<language><languageTerm type="code" authority="iso639-2b">fre</languageTerm>
<languageTerm type="code" authority="rfc3066">fr</languageTerm>
</language>
<physicalDescription></physicalDescription>
<abstract 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.</abstract>
<abstract 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.</abstract>
<subject lang="fr"><genre>keywords</genre>
<topic>Modélisation</topic>
<topic>construction de logiciels et de systèmes</topic>
<topic>vérification de propriétés</topic>
<topic>méthode B</topic>
</subject>
<subject lang="en"><genre>keywords</genre>
<topic>Modelisation</topic>
<topic>software and system construction</topic>
<topic>property verification</topic>
<topic>B method</topic>
</subject>
<relatedItem type="host"><titleInfo><title>Technique et Science Informatiques</title>
</titleInfo>
<genre type="journal" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0GLKJH51-B">journal</genre>
<subject><genre>section</genre>
<topic>SYNTHÈSE</topic>
</subject>
<identifier type="ISSN">0752-4072</identifier>
<identifier type="eISSN">2116-5920</identifier>
<identifier type="PublisherID">tsi</identifier>
<part><date>2003</date>
<detail type="volume"><caption>vol.</caption>
<number>22</number>
</detail>
<detail type="issue"><caption>no.</caption>
<number>1</number>
</detail>
<extent unit="pages"><start>89</start>
<end>118</end>
<total>30</total>
</extent>
</part>
</relatedItem>
<identifier type="istex">F0A66F68D05118BF8CCC53FBABD6958272344FED</identifier>
<identifier type="ark">ark:/67375/HT0-FLG759KZ-Q</identifier>
<identifier type="DOI">10.3166/tsi.22.00-89</identifier>
<identifier type="publisher-ID">tsi221p118</identifier>
<accessCondition type="use and reproduction" contentType="copyright">© Lavoisier SAS 2003</accessCondition>
<recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-4L897VLR-T">lavoisier</recordContentSource>
<recordOrigin>© Lavoisier SAS 2003</recordOrigin>
</recordInfo>
</mods>
<json:item><extension>json</extension>
<original>false</original>
<mimetype>application/json</mimetype>
<uri>https://api.istex.fr/ark:/67375/HT0-FLG759KZ-Q/record.json</uri>
</json:item>
</metadata>
<serie></serie>
</istex>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus

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

HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 003967 | SxmlIndent | more

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

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Istex
   |étape=   Corpus
   |type=    RBID
   |clé=     ISTEX:F0A66F68D05118BF8CCC53FBABD6958272344FED
   |texte=   B : passé, présent, futur
}}

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

B : passé, présent, futur

B : passé, présent, futur

Source :

Abstract

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