Difference between pages "Exporting and importing archives containing theories" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
(Add to Theory Plug-in category)
 
 
Line 1: Line 1:
{{TOCright}}
+
==9th Rodin User and Developer Workshop==
  
== Purpose ==
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
  
Rodin 2.0 with theory feature provides support for developing theories. But sharing theories can be somewhat difficult if care is not taken for exporting and importing them. This is related to the fact that theories are always in a particular project called "MathExtensions".
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
To understand the problem, let's say we have developed an Event-B project P and a theory T and want to make an archive in order to share them. The workspace looks like this:
 
  
+ MathExtensions
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview the ABZ2021 website] and [[#Programme|below]] (with texts).
  - T.tuf
 
  - T.dtf
 
  ...
 
  + P
 
  - C0.buc
 
  - m0.bum
 
  ...
 
  
If we make a standard archive export of these projects (File > Export > Archive File), we will get a zip file containing the project P and the project MathExtensions.
+
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.
  
But then, the person who will import the archive into his workspace with the theory feature installed (File > Import > Existing Projects into Workspace > Select archive file), will already have a project named "MathExtensions" in the workspace. Thus, the import wizard will warn that "Some projects cannot be imported because they already exist in the workspace", and theories of "MathExtensions" in the archive will not be imported. This page is dedicated to proposing workarounds for this problem.
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].  
  
== Solution 1: theories at archive root ==
+
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.
  
When exporting, select option "Create only selected directories", then select project P, but not project MathExtensions, only the T.* files in it, as shown below:
+
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.
  
[[Image:Export_P_Troot.png|500px]]
 
  
Then clean P and MathExtensions (Project > Clean).
+
=== Programme ===
  
Then, import is done in two steps:
+
'''09:00 - 10:30'''
# import T: File > Import > Archive File select the archive, untick the P project, only select T.* files at the root, select to import into the MathExtensions as shown on the image below
+
* 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]])
# import P the standard way: File > Import > Existing Projects into Workspace > Select archive file
+
* 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]], [[Media:RodinWorkshop2021_EVBT_slides.pdf|slides]])
 +
* 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]])
  
[[Image:Import_P_Troot.png|500px]]
+
'''10:30 - 11:00''' ''Break''
  
Note: in this case we chose to only put the .tuf (theory unchecked file) and .bpr (proof file) into the archive, because other files (.tcf, .bpo, .bps) are generated upon build, and .dtf (deployed theory file) is generated when deploying T. It is also possible to put every T.* files in the archive, or only T.dtf. In any case, it is generally preferable to clean imported projects and the MathExtensions project.
+
'''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]])
  
This solution is the most conservative one, as other theories that might exist in the importing workspace are conserved.
+
'''12:30--13:30''' ''Lunch''
  
== Solution 2: remove MathExtensions at import ==
+
'''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.pptx|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|slides]])
  
This second solution is the most simple but can be used only when the importer has not developed any theories.
+
=== Organisers ===
It consists in exporting P and T the standard way, so that the archive contains P and MathExtensions projects. Then the importer simply deletes his empty MathExtensions project from the workspace before importing the standard way (File > Import > Existing Projects into Workspace > Select archive file).
+
<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
 
+
<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
== Solution 3: temporary project ==
+
<p>Co-chair: Colin Snook, University of Southampton, UK</p>
 
+
<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>
This solution consists in creating a temporary project, for instance TempMathExtensions, then copying theory files to export in it. The exporter then makes a standard project archive with P and TempMathExtensions (and NOT MathExtensions).
 
 
 
The importer can then import this archive the standard way (File > Import > Existing Projects into Workspace > Select archive file), then copy theory files from TempMathExtensions to MathExtensions, and finally delete TempMathExtensions. A clean of P and MathExtensions is then highly recommended.
 
 
 
[[Category:Theory Plug-in]]
 

Revision as of 14:58, 14 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, slides)
  • 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