Difference between pages "Event-B Examples" and "Event-B XText Front-end User Guide"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>WikiSysop
 
imported>Son
 
Line 1: Line 1:
{{TOCright}}
+
== Introduction ==
This page is for listing available example Event-B/Rodin projects.
 
  
 +
The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.<br>
 +
For more details about the principles of this editor,  see [[Event-B_XText_Front-end|the Event-B XText Front-end page]].<br>
  
== Year 2009 ==
+
== Installation ==
  
=== [http://deploy-eprints.ecs.soton.ac.uk/138/ Well-ordering theorem]===  
+
=== Setup ===
By Jean-Raymond Abrial.
 
  
The slides outline the use of Rodin in the proof of Well-ordering theorem. The archive contains the
+
* Before install the Event-B XText front-end, you need to add the XText update site (http://download.eclipse.org/modeling/tmf/xtext/updates/composite/releases/) as an additional software site.
Rodin development.
+
* The Event-B XText front-end is available as a separate plug-in from the main Rodin update site (under 'Editors' category)
  
 +
=== Release Notes ===
 +
See [[Event-B_XText_Front-end_Release_Notes | Event-B XText Front-end Release Notes]]
  
=== [http://deploy-eprints.ecs.soton.ac.uk/125/ Development of a flash-based filestore]===
+
=== IMPORTANT ===
By Kriangsak Damchom and Michael Butler.
+
* Currently, Event-B XText front-end ONLY supports "standard" Event-B machines and contexts.
 +
* Since the XContexts and XMachines are compiled to the Rodin files, the corresponding Rodin contexts and machines will be '''OVER-WRITTEN'''. Any changes in the Rodin files will not be lost.
 +
* '''DO NOT USE''' the Event-B XText Front-end if you use modelling plug-ins such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.
  
The paper outlines the use of Event-B in the development of a flash-based filestore.  The archive contains the
+
== Configuration ==
Event-B development.
 
  
=== [http://deploy-eprints.ecs.soton.ac.uk/107/ Real-time controller for a water tank]===  
+
=== Event-B Explorer ===
By Michael Butler.
+
By default, XContext files (extension ''bucx'') and XMachine files (extension ''bumx'') are not display in the ''Event-B Explorer''. To enable this, select ''Customize view'' for ''Event-B Explorer'' and uncheck the option ''All files and folders''.
  
The draft paper outlines an approach to treating continuous behaviour in Event-B by a discrete approximation.
 
An example of a water tank system is used to illustrate the proposed approach.  The archive contains the
 
Event-B development for the water tank system.
 
  
=== [http://deploy-eprints.ecs.soton.ac.uk/95/ UML-B Development of an ATM]===
+
== Editing ==
By Mar Yah Said,  Michael Butler and Colin Snook.
 
  
This paper outlines support for refinement of classes and statemachines in UML-B and issustrates these
+
=== XContext ===
with an Automated Teller Machine (ATM) example. The ATM development is contained in a Rodin
+
* Any file with extension ''*.bucx'' will be recognised as XContext file. As a result, XContext file can be created by the standard ''New File'' wizard of Eclipse.
archive.  It consists of an abstract model focusing on bank account updates. The ATM, pin cards and
+
* The XText syntax of XContext file is as follows.
messaging between ATMs and a bank server are introduced in successive refinements.
+
  XContext returns econtext::Context:
 +
    {econtext::Context}
 +
    (comment=(ML_COMMENT | SL_COMMENT))?
 +
    'context' name=ID
 +
    ('extends' extends+=[econtext::Context]+)?
 +
    ('sets' sets+=XCarrierSet+)?
 +
    ('constants' constants+=XConstant+)?
 +
    ('axioms' axioms+=XAxiom+)?
 +
    'end'
 +
  ;
 +
 
 +
  XCarrierSet returns econtext::CarrierSet:
 +
    {econtext::CarrierSet}
 +
    (comment=(ML_COMMENT | SL_COMMENT))?
 +
    name=ID
 +
  ;
 +
 
 +
  XConstant returns econtext::Constant:
 +
    {econtext::Constant}
 +
    (comment=(ML_COMMENT | SL_COMMENT))?
 +
    name=ID
 +
  ;
 +
 
 +
  XAxiom returns econtext::Axiom:
 +
    {econtext::Axiom}
 +
    (comment=(ML_COMMENT | SL_COMMENT))?
 +
    name=XLABEL predicate=STRING (theorem?='theorem')?
 +
  ;
 +
 
 +
  terminal XLABEL returns ecore::EString:
 +
    '@' !(':')+ ':'
 +
  ;
  
=== [http://deploy-eprints.ecs.soton.ac.uk/84/ MIDAS: A Formally Constructed Virtual Machine]===  
+
=== XMachine ===
By [[Steve]].
+
* Any file with extension ''*.bumx'' will be recognised as XMachine file. As a result, XMachine file can be created by the standard ''New File'' wizard of Eclipse.
 +
* The XText syntax of XMachine file is as follows.
 +
  XMachine returns emachine::Machine:
 +
    {emachine::Machine}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    'machine' name=ID
 +
    ('refines' refines+=[emachine::Machine])?
 +
    ('sees' sees+=[econtext::Context]+)?
 +
    ('variables' variables+=XVariable+)?
 +
    ('invariants' invariants+=XInvariant+)?
 +
    ('variant' variant=XVariant)?
 +
    ('events' events+=XEvent (';' events+=XEvent)*)?
 +
    ('end')
 +
  ;
 +
 
 +
  XVariable returns emachine::Variable:
 +
    {emachine::Variable}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=ID
 +
  ;
 +
 
 +
  XInvariant returns emachine::Invariant:
 +
    {emachine::Invariant}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=XLABEL predicate=STRING (theorem?='theorem')?
 +
  ;
 +
 
 +
  terminal XLABEL returns ecore::EString:
 +
    '@' !(':')+ ':'
 +
  ;
 +
 
 +
  XVariant returns emachine::Variant:
 +
    {emachine::Variant}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    expression=STRING
 +
  ;
 +
 
 +
  XEvent returns emachine::Event:
 +
    {emachine::Event}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=ID
 +
    (
 +
      (extended?='extended')? &
 +
      (convergence=XConvergence)?
 +
    )
 +
    ('refines' refines+=[emachine::Event]+)?
 +
    (
 +
      ('with' witnesses+=XWitness+)?
 +
      'begin'
 +
        actions+=XAction+
 +
      'end'
 +
    |
 +
      'when'
 +
        guards+=XGuard+
 +
      ('with' witnesses+=XWitness+)?
 +
      ('then'
 +
        actions+=XAction+)?
 +
      'end'
 +
    |
 +
      'any'
 +
        parameters+=XParameter+
 +
      'where'
 +
        guards+=XGuard+
 +
      ('with' witnesses+=XWitness+)?
 +
      ('then'
 +
        actions+=XAction+)?
 +
      'end'
 +
    )?
 +
  ;
 +
 
 +
  enum XConvergence returns emachine::Convergence:
 +
    ordinary = 'ordinary' | convergent = 'convergent' | anticipated = 'anticipated';
 +
 
 +
  XParameter returns emachine::Parameter:
 +
    {emachine::Parameter}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=ID
 +
  ;
 +
 
 +
  XGuard returns emachine::Guard:
 +
    {emachine::Guard}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=XLABEL predicate=STRING (theorem?='theorem')?
 +
  ;
 +
 
 +
  XWitness returns emachine::Witness:
 +
    {emachine::Witness}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=XLABEL predicate=STRING
 +
  ;
 +
 
 +
  XAction returns emachine::Action:
 +
    {emachine::Action}
 +
    (comment=(ML_COMMENT|SL_COMMENT))?
 +
    name=XLABEL action=STRING
 +
  ;
  
MIDAS (Microprocessor Instruction and Data Abstraction System) is a specification of an Instruction Set Architecture (ISA). It is refined to a usable Virtual Machine (VM) capable of executing binary images compiled from the C language. It was developed to demonstrate a methodology for formal construction of various ISAs in Event-B via a generic model. There are two variants: a stack-based machine and a randomly accessible register array machine. The two variants employ the same instruction codes, the differences being limited to register file behavior.
+
=== Type Setting Event-B Symbols ===
 +
The Event-B Symbols are supported via Content assist, e.g., when type setting invariant or action. Sometime, a preceding blank space is required to enable the correct content assist.
  
The archive supplied at the Deploy repository contains: C-coded prototypes of the MIDAS VMs, an Event-B model refinement constructing the same VMs, the B2C Event-B to C auto-generation tool, C compiler/assembler/linkers for the VMs, an example C test suite, and execution environments for running compiled C on the machines.
+
== Converting Rodin files to Event-B XText ==
 
+
Rodin contexts and machines can be converted to XContext and XMachine files using context menu. From the ''Event-B Explorer'', right click on a Rodin project, a Rodin context, or a Rodin machine will offer option ''Convert to XText''. When a Rodin project is selected, all Rodin contexts and machines within that project will be converted.
=== [http://deploy-eprints.ecs.soton.ac.uk/82/ Development of a Network Topology Discovery Algorithm]===  
 
By ''Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond''.
 
 
 
This paper and this Rodin development is another version of the [[#Link State Routing Development|Link State Routing Development]] presented in 2008.
 
 
 
== Year 2008 ==
 
=== [http://deploy-eprints.ecs.soton.ac.uk/31/ Link State Routing Development]===
 
By ''Hoang, Thai Son and Basin, David and Kuruma, Hironobu and Abrial, Jean-Raymond''.
 
 
 
We present a formal development in Event-B of a distributed topology discovery algorithm. Distributed topology discovery is at the core several routing algorithms and is the problem of each node in a network discovering and maintaining information on the network topology. One of the key challenges in developing this algorithm is specifying the problem itself.We provide a specification that includes both safety properties, formalizing invariants that should hold in all system states, and liveness properties that characterize when the system reaches stable states. We specify these by appropriately combining invariants, event refinement, and proofs of event convergence and deadlock freedom. The combination of these features is novel and should be useful for formalizing and developing other kinds of semi-reactive systems, which are systems that react to, but do not modify, their environment.
 
 
 
=== [http://deploy-eprints.ecs.soton.ac.uk/22/ Modelling and proof of a Tree-structured File System] ===
 
By ''Damchoom, Kriangsak and Butler, Michael and Abrial, Jean-Raymond''.
 
 
 
We present a verified model of a tree-structured file system which was carried out using Event-B and the Rodin platform. The model is focused on basic functionalities affecting the tree structure including create, copy, delete and move. This work is aimed at constructing a clear and accurate model with all proof obligations discharged. While constructing the model of a file system, we begin with an abstract model of a file system and subsequently refine it by adding more details through refinement steps.  We have found that careful formulation of invariants and useful theorems that can be reused for discharging similar proof obligations make models simpler and easier to prove.
 
 
 
=== [http://deploy-eprints.ecs.soton.ac.uk/56/ Deliverable D8 D10.1 "Teaching Materials"] ===
 
By ''Abrial, Jean-Raymond and Hoang, Thai Son and Schmalz, Matthias''.
 
 
 
==Year 2007==
 
=== [http://deploy-eprints.ecs.soton.ac.uk/9/ Redevelopment of an Industrial Case Study Using Event-B and Rodin]===
 
From ''Rezazadeh, Abdolbaghi and Butler, Michael and Evans, Neil''.
 
 
 
CDIS is a commercial air traffic information system that was developed using formal methods 15 years ago by Praxis, and it is still in operation today. This system is an example of an industrial scale system that has been developed using formal methods. In particular, the functional requirements of the system were specified using VVSL -- a variant of VDM. A subset of the original specification has been chosen to be reconstructed on the Rodin platform based on the new Event-B formalism. The goal of our reconstruction was to overcome three key difficulties of the original formalisation, namely the difficulty of comprehending the original specification, the lack of any mechanical proof of the consistency of the specification and the difficulty of dealing with distribution and atomicity refinement. In this paper we elucidate how a new formal notation and tool can help to overcome these difficulties.
 
 
 
[[Category:Examples]]
 

Revision as of 18:01, 4 November 2016

Introduction

The Event-B XText front-end provides text editors for XContexts and and XMachines which then compiled automatically to Event-B contexts and machines.
For more details about the principles of this editor, see the Event-B XText Front-end page.

Installation

Setup

Release Notes

See Event-B XText Front-end Release Notes

IMPORTANT

  • Currently, Event-B XText front-end ONLY supports "standard" Event-B machines and contexts.
  • Since the XContexts and XMachines are compiled to the Rodin files, the corresponding Rodin contexts and machines will be OVER-WRITTEN. Any changes in the Rodin files will not be lost.
  • DO NOT USE the Event-B XText Front-end if you use modelling plug-ins such as iUML-B state-machines and class-diagrams, as the additional modelling elements will be over-written.

Configuration

Event-B Explorer

By default, XContext files (extension bucx) and XMachine files (extension bumx) are not display in the Event-B Explorer. To enable this, select Customize view for Event-B Explorer and uncheck the option All files and folders.


Editing

XContext

  • Any file with extension *.bucx will be recognised as XContext file. As a result, XContext file can be created by the standard New File wizard of Eclipse.
  • The XText syntax of XContext file is as follows.
 XContext returns econtext::Context:
   {econtext::Context}
   (comment=(ML_COMMENT | SL_COMMENT))?
   'context' name=ID
   ('extends' extends+=[econtext::Context]+)?
   ('sets' sets+=XCarrierSet+)?
   ('constants' constants+=XConstant+)?
   ('axioms' axioms+=XAxiom+)?
   'end'
 ;
 
 XCarrierSet returns econtext::CarrierSet:
   {econtext::CarrierSet}
   (comment=(ML_COMMENT | SL_COMMENT))?
   name=ID
 ;
 
 XConstant returns econtext::Constant:
   {econtext::Constant}
   (comment=(ML_COMMENT | SL_COMMENT))?
   name=ID
 ;
 
 XAxiom returns econtext::Axiom:
   {econtext::Axiom}	
   (comment=(ML_COMMENT | SL_COMMENT))?
   name=XLABEL predicate=STRING (theorem?='theorem')?
 ;
 
 terminal XLABEL returns ecore::EString:
   '@' !(':')+ ':'
 ;

XMachine

  • Any file with extension *.bumx will be recognised as XMachine file. As a result, XMachine file can be created by the standard New File wizard of Eclipse.
  • The XText syntax of XMachine file is as follows.
 XMachine returns emachine::Machine:
   {emachine::Machine}
   (comment=(ML_COMMENT|SL_COMMENT))?
   'machine' name=ID
   ('refines' refines+=[emachine::Machine])?
   ('sees' sees+=[econtext::Context]+)?
   ('variables' variables+=XVariable+)?
   ('invariants' invariants+=XInvariant+)?
   ('variant' variant=XVariant)?
   ('events' events+=XEvent (';' events+=XEvent)*)?
   ('end')
 ;
 
 XVariable returns emachine::Variable:
   {emachine::Variable}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=ID
 ;
 
 XInvariant returns emachine::Invariant:
   {emachine::Invariant}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=XLABEL predicate=STRING (theorem?='theorem')?
 ;
 
 terminal XLABEL returns ecore::EString:
   '@' !(':')+ ':'
 ;
 
 XVariant returns emachine::Variant:
   {emachine::Variant}
   (comment=(ML_COMMENT|SL_COMMENT))?
   expression=STRING
 ;
 
 XEvent returns emachine::Event:
   {emachine::Event}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=ID
   (
     (extended?='extended')? &
     (convergence=XConvergence)?
   )
   ('refines' refines+=[emachine::Event]+)?
   (
     ('with' witnesses+=XWitness+)?
     'begin'
       actions+=XAction+
     'end'
   |	
     'when'
       guards+=XGuard+
     ('with' witnesses+=XWitness+)?
     ('then'
       actions+=XAction+)?
     'end'
   |
     'any'
        parameters+=XParameter+
     'where'
       guards+=XGuard+
     ('with' witnesses+=XWitness+)?
     ('then'
       actions+=XAction+)?
     'end'
   )?
 ;
 
 enum XConvergence returns emachine::Convergence:
   ordinary = 'ordinary' | convergent = 'convergent' | anticipated = 'anticipated';
 
 XParameter returns emachine::Parameter:
   {emachine::Parameter}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=ID
 ;
 
 XGuard returns emachine::Guard:
   {emachine::Guard}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=XLABEL predicate=STRING (theorem?='theorem')?
 ;
 
 XWitness returns emachine::Witness:
   {emachine::Witness}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=XLABEL predicate=STRING
 ;
 
 XAction returns emachine::Action:
   {emachine::Action}
   (comment=(ML_COMMENT|SL_COMMENT))?
   name=XLABEL action=STRING
 ;

Type Setting Event-B Symbols

The Event-B Symbols are supported via Content assist, e.g., when type setting invariant or action. Sometime, a preceding blank space is required to enable the correct content assist.

Converting Rodin files to Event-B XText

Rodin contexts and machines can be converted to XContext and XMachine files using context menu. From the Event-B Explorer, right click on a Rodin project, a Rodin context, or a Rodin machine will offer option Convert to XText. When a Rodin project is selected, all Rodin contexts and machines within that project will be converted.