Difference between pages "Rodin Developer Support" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Colin
 
 
Line 1: Line 1:
−
The Developer Support provides resources for developing plug-ins for the Rodin Platform.
+
==9th Rodin User and Developer Workshop==
  
 +
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
  
−
== Rodin Developer FAQ ==
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
  
−
see [[Developer FAQ]].
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
  
−
== Architecture of the Rodin Platform ==
+
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.
  
−
=== Rodin Platform Core ===
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].
  
−
* [[Database]]
+
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.
  
−
* [[Builder]]
+
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.
  
−
* [[Rodin Index Design]]
 
  
−
* [[Indexing System]]
+
=== Programme ===
  
−
* [[Undo Redo]]
+
'''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]], [[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]])
  
−
* [[File Root Separation]]
+
'''10:30 - 11:00''' ''Break''
  
−
=== Event-B User Interface ===
+
'''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]])
  
−
The Event-B User Interface of the Roding Platform has two major components that are concerned with either [[Modelling User Interface|modelling]] in Event-B or [[Proving User Interface|proving]] properties of models.
+
'''12:30--13:30''' ''Lunch''
  
−
* [[Modelling User Interface]]
+
'''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]])
  
−
* [[Proving User Interface]]
+
=== Organisers ===
−
 
+
<p>Chair: Asieh Salehi Fathabadi, University of Southampton, UK</p>
−
Apart from these are more minor components.
+
<p>Co-chair: Thai Son Hoang, University of Southampton, UK</p>
−
 
+
<p>Co-chair: Colin Snook, University of Southampton, UK</p>
−
* [[Proof Purger Design|Proof Purger]] allows to delete unused proofs.
+
<p>Co-chair: Yamine Ait Ameur, Toulouse National Polytechnique Institute, France</p>
−
 
 
−
* [[Proof Skeleton Design]] is a view that displays skeletons of existing proofs
 
−
 
 
−
* [[Auto-Completion Design]] proposes a list of names to the user editing a model
 
−
 
 
−
=== Event-B Component Library ===
 
−
 
 
−
Event-B models and all proof-related information are stored in the Rodin database. The syntax of the mathematical notation, that is, expressions, predicates, and assignments, are maintained in an [[Abstract Syntax Tree|abstract syntax tree]]. Abstract syntax trees are manipulated by means of a class library that can be used independently of Eclipse. They are saved in the database in human-readable form as Unicode character strings. Event-B constructs, such as contexts and machines, are not represented as abstract syntax trees. They are stored and retrieved directly from the database (by contrast, mathematical formulas need additional parsing). Well-formedness of Event-B constructs is verified by a [[Static Checker|static checker]]. The static checker has two main purposes: (1) it generates error messages for ill-formed constructs, and (2) it filters well-formed parts of components to be subjected to proof obligation generation. The [[Proof Obligation Generator|proof obligation generator]] uses those parts of constructs that are well-formed and generates proof obligations from them. Finally, the [[Proof Manager|proof manager]] attempts to prove proof obligations and maintains existing proofs associated with proof obligations. The proof manager works automatically and interactively. When new proof obligations have been generated it attempts to discharge them automatically. If it does not succeed, it permits interactive proof (by means of the [[Proving User Interface|proving user interface]]).
 
−
 
 
−
* [[Abstract Syntax Tree]]
 
−
 
 
−
* [[Static Checker]]
 
−
 
 
−
* [[Proof Obligation Generator]]
 
−
 
 
−
* [[Proof Manager]]
 
−
 
 
−
* [[Proof Simplification]]
 
−
 
 
−
== Extending Rodin ==
 
−
 
 
−
* [[Developer Documentation]]
 
−
 
 
−
* [[Plug-in Tutorial]]
 
−
 
 
−
* [[Extending the Rodin Database]]
 
−
 
 
−
* [[Extending the project explorer]]
 
−
 
 
−
* [[Extending the Structure Editor]]
 
−
 
 
−
* [[Extending the Pretty Print Page]]
 
−
 
 
−
* [[Extending the Proof Manager]]
 
−
 
 
−
* [[Extending the Index Manager]]
 
−
 
 
−
* [[Extending the Static Checker]]
 
−
 
 
−
* [[Index Query]]
 
−
 
 
−
== Useful Hints ==
 
−
 
 
−
=== Version Control ===
 
−
 
 
−
All sources of the core Rodin platform (and of some plug-ins) are managed under version control in SourceForge.  The repository currently used is Subversion and can be accessed using URL [https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp  https://rodin-b-sharp.svn.sourceforge.net/svnroot/rodin-b-sharp].
 
−
 
 
−
=== Building against a version of Rodin ===
 
−
 
 
−
To develop extensions to the Rodin platform your code build needs access to a consistent (version-wise) set of Rodin platform plug-ins. (Don't just check out the latest versions from 'Head' because it may be under development and in an inconsistent state). An easy way to set up your workspace is to import the Rodin platform source code from SVN into your workspace using the 'Releng' plug-in. See [http://wiki.event-b.org/index.php/FAQ#Installing_the_sources_from_Subversion_in_Eclipse Installing the sources from Subversion in Eclipse] for further instructions.
 
−
 
 
−
Alternatively, you can set your plugin development target platform to any Rodin installation you have installed (Eclipse-Preferences-Plug-in Development-Target Platform). This is useful as a final test that everything will work once installed into Rodin but because it uses a 'built' platform, you don't get access to the Rodin source code (e.g. for de-bugging).
 
−
 
 
−
=== Testing ===
 
−
 
 
−
=== Debugging ===
 
−
 
 
−
=== Publishing ===
 
−
 
 
−
A Plug-in developed for the Rodin Platform will normally consist of a collection of eclipse 'plugin' projects and a single eclipse 'feature' project. The feature project contains branding information such as logo's icons and licensing details. It is also used to identify your Plug-in so that users can install it. To build your Plug-in use an eclipse 'site' project. This will build the jar files for your plugin projects and a jar for your feature. See eclipse documentation for more details.
 
−
 
 
−
Now you need to make your Plug-in available for users to install via the Main Rodin Update site (which comes built-in to the Rodin platform).
 
−
 
 
−
Create a new release folder in the FRS (On Sourceforge Rodin project website - Admin-file releases) noting the naming conventions (e.g. Plugin_<mypluginName>). Now you can upload your jar files using the controls on the releases webpage). Note that you should include a zip of the complete source projects to comply with Sourceforge rules.
 
−
You should not repeat files that have not changed. The Feature jar will take care of unchanged plugin jars and use the existing links. Only new jars should be included in a particular release.
 
−
See here for details:- http://alexandria.wiki.sourceforge.net/File+Release+System+-+Offering+Files+for+Download
 
−
 
 
−
Finally, the update site must be updated to redirect the update requests to the files on the FRS.
 
−
# From the sourceforge SVN repository, check out the project org.rodinp.updateSite.
 
−
# Edit the  file site.xml to add your feature and plug-in archive paths
 
−
# Test the changes by performing the install into a Rodin installation, via the local update site in your workspace.
 
−
# Commit the changes back into SVN
 
−
# Upload the new version of the update site onto the Rodin webspace. (Currently this is done by Colin Snook on request - see Rodin developers page for contact details).
 
−
 
 
−
[[Details for Maintaining Main Rodin Update Site]]
 
−
 
 
−
 
 
−
[[Category:Developer documentation]]
 
−
[[Category:Rodin Platform]]
 

Revision as of 15:17, 15 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

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