Difference between pages "User:Pascal/Collections/Deploy Deliverable D23" and "Rodin Workshop 2021"

From Event-B
< User:Pascal(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
 
Line 1: Line 1:
−
== Introduction ==
+
==9th Rodin User and Developer Workshop==
−
The purpose of this page is to provide a template to define the common content for all sections of the DEPLOY Deliverable D23 (Model Construction and Analysis Tool II), as mentioned in the [http://bscw.cs.ncl.ac.uk/bscw/bscw.cgi/d103646/D23_Writing_Plan.pdf writing plan] for this document.
 
  
−
This template takes into consideration the review feedback for the DEPLOY Deliverable D6 (Model Construction and Analysis Tool I).
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
  
−
== Template ==
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
−
For each item covered in this document (see the writing plan), a section shall be created to provide a description of work and describe the role of the WP9 partners during the passed year.  
 
  
−
=== Overview ===
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
−
This first paragraph shall identify the involved partners and give an overview of the contribution. More precisely, it shall provide answers to the following questions:
 
−
* What are the common denominations?
 
−
* Is it a new feature or an improvement?
 
−
* What are the main purposes?
 
−
* Who is in charge of the tasks?
 
−
* Who is involved among the academic and industrial partners? Who is involved as developer? Who is involved as user?
 
  
−
=== Motivations ===
+
Event-B is a formal method for system-level modelling and analysis. The
−
This paragraph shall first indicate the state before the work and highlight the encountered problems. Then, it shall express the motivation for each tool extension and improvement (requirements of industrial partners).
+
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.
  
−
=== Design Decisions ===
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].
  
−
=== Available Documentation ===
+
The purpose of this workshop  is to bring together existing and potential
−
This paragraph shall give pointers to the available wiki pages or related publications. These documents may contain:
+
users and developers of the Rodin  toolset and to foster a broader community
−
* Requirements.
+
of Rodin users and developers.
−
* Technical details (specifications).
 
−
* Teaching materials (tutorials).
 
−
* User's guides.  
 
  
−
A distinction shall be made between these categories and between documentation for developpers and documentation for end-users.
+
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.
  
−
=== Corrective and Evolutive Maintenance ===
 
−
This paragraph describes how bugs and feature requests are addressed.
 
  
−
=== Planning ===
+
=== Programme ===
−
This paragraph shall give a timeline.
 
−
More precisely, it shall give the current status of the new features (still under development, available prototype, available since release <math>M.m</math>), the current version of the features, describe the tasks which have already been completed and announce planned further work and deadlines (release versions of the Rodin platform).
 
  
−
== Formatting rules ==
+
'''09:00 - 10:30'''
−
In order to homogeneize the contributions and to ensure consistent spelling the following formatting rules shall be enforced:
+
* 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]])
−
* See §4 of [http://wiki.event-b.org/images/Llncsdoc.pdf How to Edit Your Input File] for LLNCS formatting rules.
+
* OntoEventB: A Generator of Event-B contexts from Ontologies - ''Idir Ait-Sadoune'' ([[Media:RodinWorkshop2021_OntoEventB.pdf|pdf]], [[Media:RodinWorkshop2021_OntoEventB_slides.pdf|slides]])
−
* Contractions shall not be used (eg. write "does not" instead of "doesn't", "let us" instead of "let's", etc).
+
* EVBT — an Event-B tool for code generation and documentation - ''Fredrik Öhrström'' ([[Media:RodinWorkshop2021_EVBT.pdf|pdf]])
−
* "plug-in" shall be preferred to "plugin".
+
* 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]])
  
−
== Example ==
+
'''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=User:Pascal/Collections/Deploy_Deliverable_D23&oldid=14475’