Difference between revisions of "IVOIRE Workshop 2023"

From Ivoire
Jump to navigation Jump to search
(Created page with "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?)...")
 
(→‎Schedule: Add presentations)
 
(23 intermediate revisions by the same user not shown)
Line 12: Line 12:
 
* Evaluations, benchmarkings, case studies, etc.
 
* Evaluations, benchmarkings, case studies, etc.
  
−
The IVOIRE workshop was co-located with [https://ifm22.si.usi.ch/ iFM 2022] in Lugano, Switzerland,
+
The IVOIRE workshop was co-located with [https://abz2023.loria.fr/ ABZ 2023] in Nancy, France and took place on [https://easychair.org/smart-program/ABZ2023/#session:69989 30th of May 2023].
−
took place on 7 June 2022 (the day before the main conference).
 
−
The workshop has taken place physically, like the conference itself.
 
  
−
 
+
[[File:IVOIRE Workshop 2023 Nancy.jpg||800px]]
−
[[File:IVOIRE Workshop Lugano.jpg|| 1000px]]
 
  
 
== Schedule ==
 
== Schedule ==
  
 +
The workshop took place on 30th of May 2023, 14:30–17:30.
  
−
 
+
* '''14:00–15:30''' Session 1 — ''Session Chair: Michael Leuschel''
−
* '''09:00–09:10''' Welcome note
+
** '''14:00–14:30''' ''Co-located with [https://easychair.org/smart-program/ABZ2023/#session:69988 Rodin Workshop Session III]''
−
* '''09:10–10:30''' The IVOIRE project (Session Chair: Michael Leuschel)
+
** '''14:30–14:35''' Intro to the IVOIRE project — ''Atif Mashkoor and Michael Leuschel''
−
** '''09:10–09:30''' [[Media:Atif Mashkoor - Validation obligations.pptx|Validation obligations]] (Atif Mashkoor, JKU Linz, Austria)
+
** '''14:35–15:00''' [[Media:D. Geleßus - Classification and Semantics of Validation Tasks.pdf|Classification and Semantics of Validation Tasks]] — ''David Geleßus, HHU Düsseldorf, Germany''
−
** '''09:30–09:50''' [[Media:Fabian Vu - Formalization of VOs.pdf|Formalization of VOs]] (Fabian Vu, HHU, Düsseldorf, Germany)
+
** '''15:00–15:30''' [[Media:Fabian Vu - Formalizing and Validating the VO Approach.pdf|Formalizing and Validating the VO Approach]] — ''Fabian Vu, HHU Düsseldorf, Germany''
−
** '''09:50–10:10''' [[Media:Advanced_semantics_for_VOs.pdf | Abstraction and Refinement of VOs]] (Sebastian Stock, JKU Linz, Austria)
+
* '''15:30–15:45''' Coffee break
−
** '''10:10–10:30''' IVOIRE Demo: VO Manager in ProB2-UI (David Geleßus, HHU Düsseldorf, Germany)
+
* '''15:45–17:15''' Session 2 — ''Session Chair: Atif Mashkoor''
−
* '''10:30–11:00''' ''Coffee break''
+
** '''15:45–16:15''' [[Media:Sebastian Stock - Validation-Driven Development.pdf|Validation-Driven Development]] — ''Sebastian Stock, JKU Linz, Austria''
−
* '''11:00–13:00''' B/Event-B's perspective on validation (Session Chair: Atif Mashkoor)
+
** '''16:15–16:45''' [[Media:Jean-Pierre Jacquot - A Case-study for Incremental Validation.pdf|A Case-study for Incremental Validation]] — ''Jean-Pierre Jacquot, University of Lorraine, France''
−
** '''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)
+
** '''16:45–17:15''' [[Media:Angelo Gargantini - Compositional Simulation of Abstract State Machines for Safety Critical Systems.pptx|Compositional Simulation of Abstract State Machines for Safety Critical Systems]] — ''Angelo Gargantini, University of Bergamo, Italy''
−
** '''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)
+
* '''17:15–17:30''' Wrap up
−
** '''12:00–12:30''' [[Media:Colin Snook - Behavior Driven Formal Modelling.pdf|Behavior Driven Formal Modelling]] (Colin Snook, University of Southampton, UK)
 
−
** '''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)
 
−
* '''13:00–14:30''' ''Lunch break''
 
−
* '''14:30–16:00''' ASM's perspective on validation (Session Chair: Alexander Egyed)
 
−
** '''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)
 
−
** '''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)
 
−
** '''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)
 
−
* '''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''
 
−
 
 
−
== Registration ==
 
−
 
 
−
Registration for the workshop will be handled by iFM.
 
−
See [https://ifm22.si.usi.ch/pages/registration/#other-events-7-june-2022 their registration page] for details.
 
  
 
== Organizers ==
 
== Organizers ==

Latest revision as of 07:22, 31 May 2023

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 ABZ 2023 in Nancy, France and took place on 30th of May 2023.

IVOIRE Workshop 2023 Nancy.jpg

Schedule

The workshop took place on 30th of May 2023, 14:30–17:30.

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)
Retrieved from "https://isse.jku.at/ivoire/index.php?title=IVOIRE_Workshop_2023&oldid=196"