Difference between pages "Event-B Indexers" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Laurent
 
 
Line 1: Line 1:
−
==Purpose==
+
==9th Rodin User and Developer Workshop==
  
−
Event-B indexers populate the index repository. Currently, indexers are implemented for the following files :
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
−
* machine (.bum)
 
−
* context (.buc)
 
  
 +
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
  
−
==Event-B Occurrence Kinds==
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
  
−
So far, the following occurrence kinds have been defined :
+
Event-B is a formal method for system-level modelling and analysis. The
−
* DECLARATION : when a variable, a carrier set, ..., is declared
+
Rodin Platform is an Eclipse-based toolset for Event-B that provides
−
* REFERENCE : when a variable, a carrier set, ..., is referenced (but not modified)
+
effective support for modelling and automated proof. The platform is open
−
* MODIFICATION : when a variable is modified (e.g., occurs in the left-hand side of an event action)
+
source and is further extendable with plug-ins. A range of plug-ins have
−
* REDECLARATION : when a variable, parameter or event is redeclared (refined).
+
already been developed.
−
Please notice the distinction between the index repository notion of declaration ({{class|IDeclaration}}) and the Event-B occurrence kind DECLARATION.
 
  
−
==What Is Indexed==
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].
  
−
Currently, indexed elements are :
+
The purpose of this workshop  is to bring together existing and potential
−
* carrier sets
+
users and developers of the Rodin  toolset and to foster a broader community
−
* constants
+
of Rodin users and developers.
−
* variables
 
−
* events
 
−
* parameters
 
  
−
Formulas which cannot be parsed are ignored.
+
For Rodin users the workshop will provide an opportunity to share tool
 +
experiences and to gain an understanding of on-going tool developments.
 +
For plug-in developers the workshop will provide an opportunity to showcase
 +
their tools and to achieve better coordination of tool development effort.
  
−
In the descriptions below, the following notation will be used to specify locations :
 
−
* [element] : internal location
 
−
* [element/attribute] : attribute location
 
−
* [element/attribute/begin..end] : attribute substring location
 
  
−
===Context Indexer===
+
=== Programme ===
  
−
====Dependencies====
+
'''09:00 - 10:30'''
−
* extended contexts
+
* Domain knowledge as Ontology-based Event-B Theories - ''I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque'' ([[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories.pdf|pdf]], [[Media:RodinWorkshop2021_Domain knowledge as Ontology-based Event-B Theories_slides.pdf|slides]])
 +
* OntoEventB: A Generator of Event-B contexts from Ontologies - ''Idir Ait-Sadoune'' ([[Media:RodinWorkshop2021_OntoEventB.pdf|pdf]], [[Media:RodinWorkshop2021_OntoEventB_slides.pdf|slides]])
 +
* EVBT — an Event-B tool for code generation and documentation - ''Fredrik Öhrström'' ([[Media:RodinWorkshop2021_EVBT.pdf|pdf]])
 +
* Scenario Checker: An Event-B tool for validating abstract models - ''Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Scenario Checker.pdf|pdf]], [[Media:RodinWorkshop2021_Scenario Checker_slides.pdf|slides]])
  
−
====Declarations====
+
'''10:30 - 11:00''' ''Break''
−
* carrier sets
 
−
* constants
 
  
−
====Occurrences====
+
'''11:00--12:30'''
 +
* Context instantiation plug-in: a new approach to genericity in Rodin - ''Guillaume Verdier, Laurent Voisin'' ([[Media:RodinWorkshop2021_Context instantiation plug-in.pdf|pdf]], [[Media:RodinWorkshop2021_Context instantiation plug-in_slides.pdf|slides]])
 +
* Examples of using the Instantiation Plug-in - ''Dominique Cansell, Jean-Raymond Abrial'' ([[Media:RodinWorkshop2021_Examples of using the Instantiation Plug-in.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Examples of using the Instantiation Plug-in_slides.pdf|slides]])
 +
* Data-types definitions: Use of Theory and Context instantiations Plugins - ''Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh'' ([[Media:RodinWorkshop2021_Data-types_definitions.pdf|pdf]], [[Media:RodinWorkshop2021_Data-types_definitions_slides.pdf|slides]])
 +
* Towards CamilleX 3.0 - ''Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler'' ([[Media:RodinWorkshop2021_Towards CamilleX 3.0.pdf|pdf]], [[Media:RodinWorkshop2021_Towards CamilleX 3.0_slides.pdf|slides]])
  
−
* DECLARATION of carrier sets [CarrierSet/Identifier]
+
'''12:30--13:30''' ''Lunch''
−
* DECLARATION of constants [Constant/Identifier]
 
−
* REFERENCE of elements in axioms [Axiom/Predicate/b..e]
 
−
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 
  
−
Example:
+
'''13:30--15:00'''
 +
* Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - ''Jonathan Hammond, Capgemini Engineering'' ([[Media:RodinWorkshop2021_Safety and Security Case Study Experiences with Event-B and Rodin.pdf|slides]])
 +
* Large Scale Biological Models in Rodin - ''Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre'' ([[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin.pdf|pdf]], [[Media:RodinWorkshop2021_Large Scale Biological Models in Rodin_slides.pdf|slides]])
 +
* Formal Verification of EULYNX Models Using Event-B and RODIN - ''Abdul Rasheeq, Shubhangi Salunkhe'' ([[Media:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN.pdf|pdf]], [[MEDIA:RodinWorkshop2021_Formal Verification of EULYNX Models Using Event-B and RODIN_slides.pdf|slides]])
  
−
  Ctx
+
=== Organisers ===
−
  Sets
+
<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
−
    S
+
<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
−
  Constants
+
<p>Co-chair: Colin Snook, University of Southampton, UK</p>
−
    C
+
<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>
−
  Axioms
 
−
    axm1 : C ∈ S
 
−
 
 
−
We will end up with the following occurrences :
 
−
 
 
−
  S :
 
−
    DECLARATION in [S/Identifier]
 
−
    REFERENCE in [axm1/Predicate/4..5]
 
−
  C :
 
−
    DECLARATION in [C/Identifer]
 
−
    REFERENCE in [axm1/Predicate/0..1]
 
−
 
 
−
====Exports====
 
−
* imported and declared carrier sets
 
−
* imported and declared constants
 
−
 
 
−
===Machine Indexer===
 
−
 
 
−
====Dependencies====
 
−
* refined machines
 
−
* seen contexts
 
−
 
 
−
====Declarations====
 
−
* variables
 
−
* events
 
−
* parameters
 
−
 
 
−
====Occurrences====
 
−
* DECLARATION of (local) variables [Root]
 
−
* DECLARATION of (local) events [Root]
 
−
* DECLARATION of (local) parameters [Event]
 
−
* REDECLARATION of abstract variables in the local variables that redeclare them [Variable/Identifier]
 
−
* REDECLARATION of abstract events in the local events that refine them [Event/RefinesEvent/Target]
 
−
* REDECLARATION of abstract parameters in the local parameters that redeclare them [Parameter/Identifier]
 
−
* REFERENCE of abstract parameters or variables in witnesses [Witness/Label]
 
−
* REFERENCE of elements in invariants [Invariant/Predicate/b..e]
 
−
* REFERENCE of elements in theorems [Theorem/Predicate/b..e]
 
−
* REFERENCE of elements in variants [Variant/Expression/b..e]
 
−
* REFERENCE of elements in guards [Guard/Predicate/b..e]
 
−
* REFERENCE of elements in witnesses [Witness/Predicate/b..e]
 
−
* REFERENCE of non assigned elements in actions [Action/Assignment/b..e]
 
−
* MODIFICATION of assigned elements in actions [Action/Assignment/b..e]
 
−
 
 
−
Example :
 
−
 
 
−
  M1
 
−
  VARIABLES
 
−
    var1
 
−
  INVARIANTS
 
−
    inv1 : var1 > 0
 
−
  EVENTS
 
−
    INITIALISATION
 
−
      THEN
 
−
        act1 : var1 := 1
 
−
 
 
−
After indexing M1, we will have the following occurrences:
 
−
 
 
−
  M1.var1 :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
  M1.INITIALISATION :
 
−
    DECLARATION in [M1.Root]
 
−
 
 
−
Then, if we add another machine
 
−
 
 
−
  M2
 
−
  REFINES
 
−
    M1
 
−
  VARIABLES
 
−
    var1
 
−
  EVENTS
 
−
    INITIALISATION
 
−
      THEN
 
−
        act1 : var1 := 1
 
−
 
 
−
we will add the following occurrences :
 
−
 
 
−
  M1.var1 :
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
  M2.var1 :
 
−
    DECLARATION in [M2.Root]
 
−
    MODIFICATION in [M2.act1/Assignment/0..4]
 
−
  M2.INITIALISATION :
 
−
    DECLARATION in [M2.Root]
 
−
 
 
−
====Exports====
 
−
* imported carrier sets
 
−
* imported constants
 
−
* local variables
 
−
* local events
 
−
* local parameters
 
−
 
 
−
==Propagation==
 
−
 
 
−
Propagators are defined for :
 
−
* events ({{class|EventPropagator}}) to propagate through refines
 
−
* parameters ({{class|IdentifierPropagator}}) to propagate through redeclaration
 
−
* variables ({{class|IdentifierPropagator}} as well) to propagate through redeclaration
 
−
 
 
−
In the above example with machines M1 and M2, after both files have been indexed, we can query occurrences of M1.var1.
 
−
 
 
−
With no propagator, the result would be :
 
−
 
 
−
  M1.var1 :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
 
 
−
Using the {{class|IdentifierPropagator}}, the result becomes :
 
−
 
 
−
  M1.var1 (propagated) :
 
−
    DECLARATION in [M1.Root]
 
−
    REFERENCE in [M1.inv1/Predicate/0..4]
 
−
    MODIFICATION in [M1.act1/Assignment/0..4]
 
−
    REDECLARATION in [M2.var1/Identifier]
 
−
    DECLARATION in [M2.Root]
 
−
    MODIFICATION in [M2.act1/Assignment/0..4]
 
−
 
 
−
[[Category:Developer documentation]]
 

Latest revision as of 09:41, 29 June 2021

9th Rodin User and Developer Workshop

The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)

The proceedings of the workshop is now available as a [technical report] at the University of Southampton.

The programme now available on the ABZ2021 website and below (with texts).

Event-B is a formal method for system-level modelling and analysis. The Rodin Platform is an Eclipse-based toolset for Event-B that provides effective support for modelling and automated proof. The platform is open source and is further extendable with plug-ins. A range of plug-ins have already been developed.

The 9th Rodin workshop will be collocated with the ABZ 2021 Conference.

The purpose of this workshop is to bring together existing and potential users and developers of the Rodin toolset and to foster a broader community of Rodin users and developers.

For Rodin users the workshop will provide an opportunity to share tool experiences and to gain an understanding of on-going tool developments. For plug-in developers the workshop will provide an opportunity to showcase their tools and to achieve better coordination of tool development effort.


Programme

09:00 - 10:30

  • Domain knowledge as Ontology-based Event-B Theories - I. Mendil, Y. Aït-Ameur, N. K. Singh, D. Méry, and P. Palanque (pdf, slides)
  • OntoEventB: A Generator of Event-B contexts from Ontologies - Idir Ait-Sadoune (pdf, slides)
  • EVBT — an Event-B tool for code generation and documentation - Fredrik Öhrström (pdf)
  • Scenario Checker: An Event-B tool for validating abstract models - Colin Snook, Thai Son Hoang, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

10:30 - 11:00 Break

11:00--12:30

  • Context instantiation plug-in: a new approach to genericity in Rodin - Guillaume Verdier, Laurent Voisin (pdf, slides)
  • Examples of using the Instantiation Plug-in - Dominique Cansell, Jean-Raymond Abrial (pdf, slides)
  • Data-types definitions: Use of Theory and Context instantiations Plugins - Peter Riviere, Yamine Ait-Ameur, and Neeraj Kumar Singh (pdf, slides)
  • Towards CamilleX 3.0 - Thai Son Hoang, Colin Snook, Asieh Salehi Fathabadi, Dana Dghaym, Michael Butler (pdf, slides)

12:30--13:30 Lunch

13:30--15:00

  • Keynote: Safety and Security Case Study Experiences with Event-B and Rodin - Jonathan Hammond, Capgemini Engineering (slides)
  • Large Scale Biological Models in Rodin - Usman Sanwal, Thai Son Hoang, Luigia Petre, and Ion Petre (pdf, slides)
  • Formal Verification of EULYNX Models Using Event-B and RODIN - Abdul Rasheeq, Shubhangi Salunkhe (pdf, slides)

Organisers

Chair: Asieh Salehi Fathabadi, University of Southampton, UK

Co-chair: Thai Son Hoang, University of Southampton, UK

Co-chair: Colin Snook, University of Southampton, UK

Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France

Retrieved from ‘https://wiki.event-b.org/index.php?title=Event-B_Indexers&oldid=14475’