InforLorV4, Main, Merge, bibRecord, 006596

Refinement and reachability in Event―B

Identifieur interne : 006596 ( Main/Merge ); précédent : 006595; suivant : 006597

Refinement and reachability in Event―B

Auteurs : Jean-Raymond Abrial [Suisse] ; Dominique Cansell [France] ; Dominique Méry [France]

Source :

Lecture notes in computer science [ 0302-9743 ] ; 2005.

RBID : Pascal:05-0288511

Descripteurs français

Pascal (Inist)
- Développement logiciel, Spécification formelle, Non déterminisme, Système non déterministe, Logique temporelle, Raffinage, Méthode raffinement, Atteignabilité, Approche probabiliste, Invariant.

English descriptors

KwdEn :
- Formal specification, Invariant, Non determinism, Non deterministic system, Probabilistic approach, Reachability, Refinement method, Refining, Software development, Temporal logic.

Abstract

Since the early 90's (after the seminal article of R. Back [4]), the refinement of stuttering steps [5] are performed by means of new actions (called here events) refining skip. It is shown in this article that such a refinement method is not always possible in the development of large systems. We shall instead use events refining some kind of non-deterministic actions maintaining the invariant (sometimes called keep). We show that such new refinements are completely safe. In a second part, we explain how such a mechanism can be used to express some reachability conditions that were otherwise expressed using some special temporal logic statements à la TLA [5] in a previous article [2]. Examples will be used to illustrate our proposals.

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000556
to stream PascalFrancis, to step Curation: 000482
to stream PascalFrancis, to step Checkpoint: 000459

Links to Exploration step

Pascal:05-0288511

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">Refinement and reachability in Event―B</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"><inist:fA14 i1="01"><s1>ETHZ Zurich</s1>
<s3>CHE</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Suisse</country>
<wicri:noRegion>ETHZ Zurich</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="4"><inist:fA14 i1="02"><s1>LORIA, Université de Metz</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Université de Metz</wicri:noRegion>
<placeName><settlement type="city">Metz</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Paul Verlaine - Metz</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="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LORIA, Université Henri Poincaré Nancy 1</s1>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Université Henri Poincaré Nancy 1</wicri:noRegion>
<wicri:noRegion>LORIA, Université Henri Poincaré Nancy 1</wicri:noRegion>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">05-0288511</idno>
<date when="2005">2005</date>
<idno type="stanalyst">PASCAL 05-0288511 INIST</idno>
<idno type="RBID">Pascal:05-0288511</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000556</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000482</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000459</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000459</idno>
<idno type="wicri:doubleKey">0302-9743:2005:Abrial J:refinement:and:reachability</idno>
<idno type="wicri:Area/Main/Merge">006596</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">Refinement and reachability in Event―B</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"><inist:fA14 i1="01"><s1>ETHZ Zurich</s1>
<s3>CHE</s3>
<sZ>1 aut.</sZ>
</inist:fA14>
<country>Suisse</country>
<wicri:noRegion>ETHZ Zurich</wicri:noRegion>
</affiliation>
</author>
<author><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
<affiliation wicri:level="4"><inist:fA14 i1="02"><s1>LORIA, Université de Metz</s1>
<s3>FRA</s3>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Université de Metz</wicri:noRegion>
<placeName><settlement type="city">Metz</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="university">Université Paul Verlaine - Metz</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="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
<author><name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
<affiliation wicri:level="1"><inist:fA14 i1="03"><s1>LORIA, Université Henri Poincaré Nancy 1</s1>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<wicri:noRegion>Université Henri Poincaré Nancy 1</wicri:noRegion>
<wicri:noRegion>LORIA, Université Henri Poincaré Nancy 1</wicri:noRegion>
<placeName><settlement type="city">Nancy</settlement>
<region type="region" nuts="2">Grand Est</region>
<region type="region" nuts="2">Lorraine (région)</region>
</placeName>
<orgName type="team" n="7">Mosel (Loria)</orgName>
<orgName type="lab">Laboratoire lorrain de recherche en informatique et ses applications</orgName>
<orgName type="university">Université de Lorraine</orgName>
<orgName type="EPST">Centre national de la recherche scientifique</orgName>
<orgName type="EPST">Institut national de recherche en informatique et en automatique</orgName>
</affiliation>
</author>
</analytic>
<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>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Formal specification</term>
<term>Invariant</term>
<term>Non determinism</term>
<term>Non deterministic system</term>
<term>Probabilistic approach</term>
<term>Reachability</term>
<term>Refinement method</term>
<term>Refining</term>
<term>Software development</term>
<term>Temporal logic</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Développement logiciel</term>
<term>Spécification formelle</term>
<term>Non déterminisme</term>
<term>Système non déterministe</term>
<term>Logique temporelle</term>
<term>Raffinage</term>
<term>Méthode raffinement</term>
<term>Atteignabilité</term>
<term>Approche probabiliste</term>
<term>Invariant</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Since the early 90's (after the seminal article of R. Back [4]), the refinement of stuttering steps [5] are performed by means of new actions (called here events) refining skip. It is shown in this article that such a refinement method is not always possible in the development of large systems. We shall instead use events refining some kind of non-deterministic actions maintaining the invariant (sometimes called keep). We show that such new refinements are completely safe. In a second part, we explain how such a mechanism can be used to express some reachability conditions that were otherwise expressed using some special temporal logic statements à la TLA [5] in a previous article [2]. Examples will be used to illustrate our proposals.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Suisse</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
</region>
<settlement><li>Metz</li>
<li>Nancy</li>
</settlement>
<orgName><li>Centre national de la recherche scientifique</li>
<li>Institut national de recherche en informatique et en automatique</li>
<li>Laboratoire lorrain de recherche en informatique et ses applications</li>
<li>Mosel (Loria)</li>
<li>Université Paul Verlaine - Metz</li>
<li>Université de Lorraine</li>
</orgName>
</list>
<tree><country name="Suisse"><noRegion><name sortKey="Abrial, Jean Raymond" sort="Abrial, Jean Raymond" uniqKey="Abrial J" first="Jean-Raymond" last="Abrial">Jean-Raymond Abrial</name>
</noRegion>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Cansell, Dominique" sort="Cansell, Dominique" uniqKey="Cansell D" first="Dominique" last="Cansell">Dominique Cansell</name>
</region>
<name sortKey="Mery, Dominique" sort="Mery, Dominique" uniqKey="Mery D" first="Dominique" last="Mery">Dominique Méry</name>
</country>
</tree>
</affiliations>
</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 006596 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Merge/biblio.hfd -nk 006596 | 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é=     Pascal:05-0288511
   |texte=   Refinement and reachability in Event―B
}}

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

Refinement and reachability in Event―B

Refinement and reachability in Event―B

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

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