Refinement and Reachability in Event_B

Jean-Raymond Abrial; Dominique Cansell; Dominique Méry

inria-00001245, version 1

Refinement and Reachability in Event_B

Jean-Raymond Abrial ¹, Dominique Cansell () ^2, 3, Dominique Méry ²

ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users 3455 (2005) 222-241

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.

1: Department of Computer Science (ETH Zurich)
ETH Zurich
2: MOSEL (INRIA Lorraine - LORIA)
INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
3: Université de Metz (UNIVERSITÉ DE METZ)
Université de Metz

inria-00001245, version 1
http://hal.inria.fr/inria-00001245
oai:hal.inria.fr:inria-00001245
From: Publications Loria <>
Submitted on: Tuesday, 11 April 2006 17:38:31
Updated on: Friday, 30 June 2006 16:43:44

See detailed view

Associated documents

DOI: 10.1007/11415787_14

Export

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="inproceedings"><head>Peer-reviewed conferences/proceedings</head>
<biblStruct type="inproceedings" xml:id="inria-00001245"><analytic>
<author><persName><forename>Jean-Raymond</forename><surname>Abrial</surname></persName>
<affiliation>
<orgName type="laboratory">ETH Zurich</orgName>
<orgName type="team">Department of Computer Science</orgName>
<country>CH</country>
<orgName type="institution">ETH Zurich</orgName>
</affiliation>
</author>
<author><persName><forename>Dominique</forename><surname>Cansell</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">UNIVERSITÉ DE METZ</orgName>
<orgName type="team">Université de Metz</orgName>
<country>FR</country>
<orgName type="institution">Université de Metz</orgName>
</affiliation>
</author>
<author><persName><forename>Dominique</forename><surname>Méry</surname></persName>
<affiliation>
<orgName type="laboratory">INRIA Lorraine - LORIA</orgName>
<orgName type="team">MOSEL</orgName>
<country>FR</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">CNRS : UMR7503</orgName>
<orgName type="institution">Université Henri Poincaré - Nancy I</orgName>
<orgName type="institution">Université Nancy II</orgName>
<orgName type="institution">Institut National Polytechnique de Lorraine (INPL)</orgName>
</affiliation>
</author>
<title type="main" level="a">Refinement and Reachability in Event_B</title></analytic><monogr><meeting>ZB 2005 : Formal Specification and Development in Z and B : 4th International Conference of B and Z Users</meeting><imprint><publisher>Springer</publisher><pubPlace><settlement>Guilford</settlement><country>UK</country></pubPlace><biblScope type="publicationDate">2005-04-00</biblScope><biblScope type="vol">3455</biblScope><biblScope type="pp">222-241</biblScope></imprint></monogr><idno type="doi">10.1007/11415787_14</idno><idno type="HALid">http://hal.inria.fr/inria-00001245</idno></biblStruct>
</listBibl>
</listBibl>