Difference between pages "Strengthening the AST Library for Rodin 3.0" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Vinmont
 
 
Line 1: Line 1:
−
A part of the Rodin 3.0 development aims to strengthen the AST library. This page explains the choices we have done during this step.
+
==9th Rodin User and Developer Workshop==
  
−
== Type Environment ==
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
−
Type environments have changed in Rodin 3.0 in order to reinforce their good use and their robustness.
 
−
First of all we add a new mechanism to add given sets implicitly introduced by types when new elements are added.
 
−
Then we create the inferred type environment Java type to could differentiate a classical type environment and an inferred one which now references its initial type environment. This type is now used in the type checking result. Since an inferred type environment content depends on its initial type environment it was a necessary modification to could express all possible inferred type environments.
 
−
Finally we add mechanism to separate mutable and immutable type environments by creating two children interfaces of the type environment interface, {{class|ITypeEnvironmentBuilder}} and {{class|ISealedTypeEnvironment}}. This mechanism provides a strong guarantee that a type environment will not be modified if necessary and allows at the same time to be flexible when it is needed (see [[Rodin 3.0 Plug-in Migration Guide]] for more information).
 
  
−
== Type Checking ==
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
−
The type checking step has been strengthened to avoid that the type checker accepts given types implicitly introducing given sets incompatibles with the type environment and thus free identifiers. It also allowed to detect and correct a new occurrence of the bug #635 (old name #3574565) that was leading on a incoherent result of the formula type checking since the formula was not correctly type checked but the result was indicating a success.
 
  
−
Regarding the legibility for identifiers no modification has been done, that is to say that if the same name is used for a free and bound identifiers then the bound identifier will be renamed since it is identified by its Bruijn number.
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
  
−
The modification of the type checking step introduces the following modifications:
+
Event-B is a formal method for system-level modelling and analysis. The
−
* In the ''typecheck()'' procedure of nodes, we now analyse the type of the nodes that could introduce new given sets and add those given sets to the resulting inferred type environment. It guarantees that incompatible free identifiers names or given sets are not introduced.
+
Rodin Platform is an Eclipse-based toolset for Event-B that provides
−
* In the ''synthesize()'' procedure, that is executed a first time at node creation and a second time during solving types step, we now add the given sets introduced by given types as free identifiers on concerned nodes. As a consequence if a given set and a free identifier have a name conflict it will also be detected during this step. Particularly it will provide a way to detect and raise an {{class|IllegalArgumentException}} when an invalid type is provided at node creation.
+
effective support for modelling and automated proof. The platform is open
−
* If the whole type checking procedure succeeds then all free identifiers are checked and added to the inferred environment if necessary.
+
source and is further extendable with plug-ins. A range of plug-ins have
 +
already been developed.
  
−
== AST nodes construction ==
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].  
−
AST nodes construction is possible using {{class|FormulaFactory}} methods (direct access to constructors is now explicitly forbidden) and has been strengthened by verifying that arguments provided are valid regarding constructed node. Those verifications are documented with the exceptions raised when conditions on arguments are not respected. It allow to avoid exceptions raised later for which source is more complicated to locate.
 
  
−
[[Category:Design]]
+
The purpose of this workshop  is to bring together existing and potential
−
[[Category:Developer documentation]]
+
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'' ([[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]])
 +
 
 +
'''10:30 - 11:00''' ''Break''
 +
 
 +
'''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]])
 +
 
 +
'''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'' ([[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]])
 +
 
 +
=== Organisers ===
 +
<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
 +
<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
 +
<p>Co-chair: Colin Snook, University of Southampton, UK</p>
 +
<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>

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=Strengthening_the_AST_Library_for_Rodin_3.0&oldid=14475’