Difference between revisions of "IVOIRE Workshop 2022"

From Ivoire
Jump to navigation Jump to search
 
(28 intermediate revisions by the same user not shown)
Line 4: Line 4:
  
 
The [[Main Page|IVOIRE project]] focuses on developing an enhanced formal paradigm based on an extension of the refinement framework that includes a comprehensive validation process and toolchain to perform validation obligations.
 
The [[Main Page|IVOIRE project]] focuses on developing an enhanced formal paradigm based on an extension of the refinement framework that includes a comprehensive validation process and toolchain to perform validation obligations.
The main goal of this workshop is to provide a platform for formal methods practitioners, researchers, and academics to discuss various issues associated with validation for formal methods,
+
The main goal of this workshop was to provide a platform for formal methods practitioners, researchers, and academics to discuss various issues associated with validation for formal methods,
 
including but not limited to:
 
including but not limited to:
  
Line 12: Line 12:
 
* Evaluations, benchmarkings, case studies, etc.
 
* Evaluations, benchmarkings, case studies, etc.
  
The IVOIRE workshop will be co-located with [https://ifm22.si.usi.ch/ iFM 2022] in Lugano, Switzerland,
+
The IVOIRE workshop was co-located with [https://ifm22.si.usi.ch/ iFM 2022] in Lugano, Switzerland,
taking place on 7 June 2022 (the day before the main conference).
+
took place on 7 June 2022 (the day before the main conference).
The workshop is currently planned to take place physically, like the conference itself.
+
The workshop has taken place physically, like the conference itself.
 +
 
 +
 
 +
[[File:IVOIRE Workshop Lugano.jpg|| 1000px]]
  
 
== Schedule ==
 
== Schedule ==
  
* '''09:00–09:15''' Welcome note by Michael Leuschel (HHU, Germany) and Atif Mashkoor (JKU, Austria)
+
 
* '''09:15–10:15''' IVOIRE Theory:  
+
 
** '''09:15–09:35''' Introduction: Validation Obligations
+
* '''09:00–09:10''' Welcome note
** '''09:35–09:55''' Refinement of VOs, Abstraction + Nonlinear Refinement
+
* '''09:10–10:30''' The IVOIRE project (Session Chair: Michael Leuschel)
** '''09:55–10:15''' IVOIRE Demo: ProB2-UI (+ VO Manager)
+
** '''09:10–09:30''' [[Media:Atif Mashkoor - Validation obligations.pptx|Validation obligations]] (Atif Mashkoor, JKU Linz, Austria)
* '''10:15–10:45''' ''Coffee break''
+
** '''09:30–09:50''' [[Media:Fabian Vu - Formalization of VOs.pdf|Formalization of VOs]] (Fabian Vu, HHU, Düsseldorf, Germany)
* '''10:45–12:25''' B/Event-B's perspective on validation
+
** '''09:50–10:10''' [[Media:Advanced_semantics_for_VOs.pdf | Abstraction and Refinement of VOs]] (Sebastian Stock, JKU Linz, Austria)
** '''10:45–11:15''' Jean-Pierre Jacquot (University of Lorraine, France)
+
** '''10:10–10:30''' IVOIRE Demo: VO Manager in ProB2-UI (David Geleßus, HHU Düsseldorf, Germany)
** '''11:15–11:45''' Richard Banach (University of Manchester, UK)
+
* '''10:30–11:00''' ''Coffee break''
** '''11:45–12:15'''
+
* '''11:00–13:00''' B/Event-B's perspective on validation (Session Chair: Atif Mashkoor)
* '''12:15–14:00''' ''Lunch break''
+
** '''11:00–11:30''' [[Media:Jean-Pierre Jacquot - Validation An Event-B perspective with JeB.pdf|Validation: An Event-B perspective with JeB]] (Jean-Pierre Jacquot, University of Lorraine, France)
* '''14:00–15:30''' ASM's perspective on validation
+
** '''11:30–12:00''' [[Media:Richard Banach - Graded Refinement, Retrenchment and Simulation, for Challenging Requirements.pdf|Graded Refinement, Retrenchment and Simulation, for Challenging Requirements]] (Richard Banach, University of Manchester, UK)
** '''14:00–14:30''' Egon Börger (University of Pisa, Italy)
+
** '''12:00–12:30''' [[Media:Colin Snook - Behavior Driven Formal Modelling.pdf|Behavior Driven Formal Modelling]] (Colin Snook, University of Southampton, UK)
** '''14:30–15:00''' Angelo Gargantini (University of Bergamo, Italy)
+
** '''12:30–13:00''' [[Media:Dominique Méry - Refinement-based Construction of Correct IoT Protocols.pdf|Refinement-based Construction of Correct IoT Protocols]] (Dominique Méry, University of Lorraine, France)
** '''15:00–15:30''' Elvinia Riccobene (University of Milan, Italy)
+
* '''13:00–14:30''' ''Lunch break''
* '''15:30–16:00''' ''Coffee break''
+
* '''14:30–16:00''' ASM's perspective on validation (Session Chair: Alexander Egyed)
* '''16:00–17:00''' Industrial perspective on validation
+
** '''14:30–15:00''' [[Media:Egon Börger - The ASM Method Integrates Validation and Verification at Different Abstraction Levels.pdf|The ASM Method Integrates Validation and Verification at Different Abstraction Levels]] (Egon Börger, University of Pisa, Italy)
** '''16:00–16:30''' Thierry Lecomte (Clearsy, France)
+
** '''15:00–15:30''' [[Media:Angelo Gargantini - On the importance of scenario-based validation.pptx|On the importance of scenario-based validation]] (Angelo Gargantini, University of Bergamo, Italy)
** '''16:30–17:00'''
+
** '''15:30–16:00''' [[Media:Elvinia Riccobene - Exploiting the advantage of formal executable models@RUNTIME.pdf|Exploiting the advantage of formal executable models@RUNTIME]] (Elvinia Riccobene, University of Milan, Italy)
* '''17:00–18:00''' Discussion and concluding remarks
+
* '''16:00–16:30''' ''Coffee break''
 +
* '''16:30–17:00''' Industrial perspective on validation (Session Chair: Michael Leuschel)
 +
** '''16:30–17:00''' [[Media:Alexander Egyed - DesignSpace for collaborative engineering.pdf|DesignSpace for collaborative engineering]] (Alexander Egyed, JKU Linz, Austria)
 +
** [[Media:Thierry Lecomte - Methodology for formal proof of spec.pdf|Methodology for formal proof of specification]] (Thierry Lecomte, CLEARSY, France)
 +
* '''17:00–17:30''' Discussion and concluding remarks
 
* '''19:30''' ''Workshop dinner''
 
* '''19:30''' ''Workshop dinner''
  

Latest revision as of 09:07, 14 June 2022

Historically, formal methods and supported environments have focused more on only one-half of the quality-assurance process: verification (are we building the software right?). The other half, validation (are we building the right software?) has been given much less attention, i.e., we have fewer automated/push-button tools available for validation, unlike verification.

The IVOIRE project focuses on developing an enhanced formal paradigm based on an extension of the refinement framework that includes a comprehensive validation process and toolchain to perform validation obligations. The main goal of this workshop was to provide a platform for formal methods practitioners, researchers, and academics to discuss various issues associated with validation for formal methods, including but not limited to:

  • Validation obligations or other systematic approaches to validation
  • Relation between refinement and validation, and the interplay between verification and validation
  • Environments and tools to manage the validation process
  • Evaluations, benchmarkings, case studies, etc.

The IVOIRE workshop was co-located with iFM 2022 in Lugano, Switzerland, took place on 7 June 2022 (the day before the main conference). The workshop has taken place physically, like the conference itself.


IVOIRE Workshop Lugano.jpg

Schedule

Registration

Registration for the workshop will be handled by iFM. See their registration page for details.

Organizers

Workshop chairs:

  • Atif Mashkoor (JKU Linz, Austria)
  • Michael Leuschel (HHU Düsseldorf, Germany)

Workshop organizing committee:

  • Sebastian Stock (JKU Linz, Austria)
  • Fabian Vu (HHU Düsseldorf, Germany)
  • David Geleßus (HHU Düsseldorf, Germany)