Difference between pages "Event-B to SMT-LIB" and "Rodin Workshop 2021"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
 
Line 1: Line 1:
−
{{TOCright}}
+
==9th Rodin User and Developer Workshop==
  
−
== Introduction ==
+
The 9th Rodin User and Developer Workshop, 8 June, 2021, Ulm, Germany (Virtual)
−
The Event-B to [[#ancre_3|SMT-LIB]] plug-in allows to translate mathematical lemmas that rely on the Event-B language to the SMT-LIB format.
 
  
−
The considered lemmas are those often encountered in practice, but not yet well supported by proving
+
''The proceedings of the workshop is now available as a [technical report] at the University of Southampton.''
−
tools such as those embedded in the Rodin platform. The purpose is not here to entirely define the translation, but rather to give a mapping for this subset of Event-B formulas. These typical mathematical problems are entry points for the [[#ancre_1|DECERT]] project, and more precisely for the Work Package 1. Using the SMT-LIB standard is among the requirements for this project.
 
  
−
This version mainly focuses on lemmas based on unquantified integer linear arithmetic.
+
The programme now available on [https://abz2021.uni-ulm.de/program-overview  the ABZ2021 website] and [[#Programme|below]] (with texts).
  
−
== Specification ==
+
Event-B is a formal method for system-level modelling and analysis. The
−
A first [[#ancre_2|specification draft]] has been written.
+
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.
  
−
== Implementation ==
+
The 9th Rodin workshop will be collocated with the [https://abz2021.uni-ulm.de/ ABZ 2021 Conference].  
−
A first plug-in prototype is accessible under the following respositories:
 
−
* <tt>_exploratory/carinepascal/fr.systerel.decert</tt>
 
−
* <tt>_exploratory/carinepascal/fr.systerel.decert.tests</tt>
 
  
−
The following theories are currently supported: Linear Arithmetic, Linear Order and Integer. The lemmas referencing other theories will not be translated.
+
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.
  
−
== How to perform the translation? ==
+
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.
  
−
The XML files containing the Event-B lemmas are assumed to be stored in the <tt>Lemmas</tt> folder. The SMT files containing the SMT-LIB benchmarks are assumed to be stored in the <tt>Benchmarks</tt> folder.
 
  
−
Follow the following steps in order to translate Event-B lemmas to SMT-LIB benchmarks:
+
=== Programme ===
−
<ol>
 
−
<li> Launch the <tt>fr.systerel.decert.tests.TypeCheckingTests</tt> JUnit test to type-check the lemmas (optional).
 
−
Note that it is previously necessary to set the <tt>XMLFolder</tt> field of the <tt>TypeCheckingTests</tt> class to specify the absolute path of the <tt>Lemmas</tt> folder.
 
  
−
<li> Launch the <tt>fr.systerel.decert.tests.smt.TranslationTests</tt> JUnit test to translate the lemmas (mandatory).  
+
'''09:00 - 10:30'''
−
Note that it is necessary to previously configure the test:
+
* 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 <tt>XMLFolder</tt> field shall contain the absolute path of the <tt>Lemmas</tt> folder.
+
* OntoEventB: A Generator of Event-B contexts from Ontologies - ''Idir Ait-Sadoune'' ([[Media:RodinWorkshop2021_OntoEventB.pdf|pdf]], [[Media:RodinWorkshop2021_OntoEventB_slides.pdf|slides]])
−
* The <tt>SMTFolder</tt> field shall contain the absolute path of the <tt>Benchmarks</tt> folder.
+
* EVBT — an Event-B tool for code generation and documentation - ''Fredrik Öhrström'' ([[Media:RodinWorkshop2021_EVBT.pdf|pdf]])
−
* If the format of the generated SMT files is to be checked, the <tt>CHECK_FORMAT</tt> option shall be set and the <tt>SMTParserFolder</tt> field shall contain the absolute path of the directory where is installed the SMT-LIB parser. Otherwise, the option shall be turned off. The SMT-LIB parser is available from the [http://goedel.cs.uiowa.edu/smtlib SMT-LIB web page].
+
* 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]])
−
* If the generated benchmarks are to be checked for satisfiability, the <tt>CHECK_SAT</tt> option shall be set and the <tt>SMTSolverFolder</tt> field shall contain the absolute path of the directory where is installed the Z3 SMT solver. Otherwise, the option shall be turned off. The Z3 SMT solver is available from the [http://research.microsoft.com/en-us/um/redmond/projects/z3 following address].
 
−
</ol>
 
  
−
== Bibliography ==
+
'''10:30 - 11:00''' ''Break''
−
* <font id="ancre_1">DECERT</font>, [http://decert.gforge.inria.fr/index.html ''DEduction and CERTification'']
 
−
* C. Pascal, [http://wiki.event-b.org/images/B2SMTLIB.pdf <font id="ancre_2">''From Event-B lemmas to SMT-LIB benchmarks''</font>], May 2009.
 
−
* S. Ranise and C. Tinelli, [http://goedel.cs.uiowa.edu/smtlib/papers/format-v1.2-r06.08.30.pdf <font id="ancre_3">''The SMT-LIB standard''</font>], Version 1.2, 2006, 2006.
 
  
−
[[Category:Design]]
+
'''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=Event-B_to_SMT-LIB&oldid=14475’