Difference between pages "D45 Scalability" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Tommy
 
 
Line 1: Line 1:
−
= Overview =
+
==9th Rodin User and Developer Workshop==
−
* '''Improved Performance''' According to the refocus mentionned in the [[D45_General_Platform_Maintenance#Motivations| General Platform Maintenance]] chapter, much of the reworking efforts performed on the core plateform basically aimed to overcome Rodin scalability weaknesses, and the continuous need of seamless proving experience. The whole performance was enhanced by core implementation and user interface refactorings. Improvements made to the proving experience will be detailed in a separate chapter.
 
−
* {{TODO}} An overview of the contribution about the design pattern management / Generic Instantiation (Thai Son Hoang)
 
−
* '''Edition''' It appeard along DEPLOY, the models defined by pilots becoming industrial sized due to the level of complexity reached, that the edition became a central concern.
 
−
:*The legacy structured editor based on a form edition specific achitecture reach its limits in responsivness and hence in usability when being constrained to display a huge amount of graphical elements.
 
−
:*Camille textual editor had to tackle challenges related to ressources mapping and management for projects of industrial size mentionned above or even the design of extension capabilities, that became a major concern since the grammar could be extended with theories.
 
  
−
= Motivations =
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
  
−
== Improved Performance ==
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
−
It appeared that the various DEPLOY partners encountered several major issues while editing large models. Some were related to the core code of the Rodin platform, causing crashes, loss of data, corruption in models. Some other were related to the UI causing platform hanging, and sometimes leading to its freezing which required sometimes to kill the Rodin process, thus also leading to potential loss of data and corruption in models. Hence, it appeared necessary to solve such issues before the end of DEPLOY.
 
  
−
== Design Pattern Management / Generic Instantiation  ==
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
−
{{TODO}} ''To be completed by Thai Son Hoang''
 
−
== Edition ==
 
−
* The motivations behind the creation of the new textual structured editor mainly concern performance but not only. From the growing size of complexity reached in models inducing a growing of their physical size lead the platform to its limits. Two major kinds of failures were faced when developing such models:
 
−
:* failures occuring on windows platforms, the mostly used system, when reaching the operating system limit number of graphical elements in memory allowed to be displayed at once. This bug used to crash the Rodin platform, and it appeared necessary to control the number of graphical elements needed to display the model elements. Architectures sparing these graphical elements should be thus favoured.
 
−
:* failures due to the high consumption of memory by the heavy graphical elements used by the forms of legacy editor.
 
−
Moreover, it appeared important to visualize some elements that are not part of the current level of modelling, but are linked to it. These elements are called the "inherited" elements, or "implicit children". The legacy structured editor being directly interfaced with the underlying Event-B models in database, it was difficult and tricky to display inherited elements. Hence, it was one more argument to go for a new editor, this time based on a intermediary representation of the models.
 
  
−
* The motivations about Camille evolution {{TODO}} Ingo Weigelt.
+
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.
  
−
= Choices / Decisions =
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].  
−
== Improved Performance ==
 
−
SYSTEREL lead a two phase investigation to have a better idea of the work to be done. Each phase being followed by some refactoring of the code. Out of the early investigation, a cause and effect relationship has been found between perfomance loss and the various reported bugs, such as "platform hanging" bugs or even "no more handle" bugs related to the high consumption of graphical elements on Windows platforms. Indeed, it appeared that solving the performance issues sometimes solved induced bugs as well which made the scalability improvement tasks emcompass the maintenance goals.<br>
 
−
Later, a deeper investigation was performed, to indentify and tackle the remaining performance issues. Profiling and code review were the two techniques used. The profiling strategy allowed to get a better localisation of the performance loss in both UI and core code while the code review helped to understand the intrinsic misuses or drawbacks of particular components and/or architectures.
 
−
A good example, was the Event-B built-in editor based on form editors with a high use of greedy graphical components. Such architecture appeard to be weak when it was needed to display industrial size models. This affected the modelling experience with some long, and really annoying to the user, reaction lags. To solve such issue, it has been chosen to refactor the editors using a textual representation which was a light-weight graphical alternative to lower the number of needed components.
 
  
−
== Design Pattern Management / Generic Instantiation ==
+
The purpose of this workshop is to bring together existing and potential
−
{{TODO}} ''To be completed by Thai Son Hoang''
+
users and developers of the Rodin  toolset and to foster a broader community
−
== Edition ==
+
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.
  
−
* About the Text Editor {{TODO}} Ingo Weigelt
 
  
−
= Available Documentation =
+
=== Programme ===
−
* {{TODO}} Links for Improved Performance
 
−
* {{TODO}} Links for Design Pattern Management / Generic Instantiation
 
−
* {{TODO}} Links for Edition
 
  
−
= Status =
+
'''09:00 - 10:30'''
−
== Improved Performance ==
+
* 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]])
−
The refactoring made on both core code and UI code allowed to gain up to 25 times speed-up on the UI, and almost a 2 times speed-up in the core code, making the platform usable in an industrial sized context.<br>
+
* 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]])
  
−
== Design Pattern Management / Generic Instantiation  ==
+
'''10:30 - 11:00''' ''Break''
−
{{TODO}} ''To be completed by Thai Son Hoang''
 
−
== Edition ==
 
−
{{TODO}} ''To be completed by Thomas Muller, Ingo Weigelt''
 
  
 +
'''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]])
  
−
= References =
+
'''12:30--13:30''' ''Lunch''
−
<references/>
 
  
−
[[Category:D45 Deliverable]]
+
'''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=D45_Scalability&oldid=14475’