IVOIRE Workshop 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 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.

Schedule

• 09:00–09:10 Welcome note
• 09:10–10:30 The IVOIRE project (Session Chair: Michael Leuschel)
  • 09:10–09:30 Validation obligations (Atif Mashkoor, JKU Linz, Austria)
  • 09:30–09:50 Formalization of VOs (Fabian Vu, HHU, Düsseldorf, Germany)
  • 09:50–10:10 Abstraction and Refinement of VOs (Sebastian Stock, JKU Linz, Austria)
  • 10:10–10:30 IVOIRE Demo: VO Manager in ProB2-UI (David Geleßus, HHU Düsseldorf, Germany)
• 10:30–11:00 Coffee break
• 11:00–13:00 B/Event-B's perspective on validation (Session Chair: Atif Mashkoor)
  • 11:00–11:30 Validation: An Event-B perspective with JeB (Jean-Pierre Jacquot, University of Lorraine, France)
  • 11:30–12:00 Graded Refinement, Retrenchment and Simulation, for Challenging Requirements (Richard Banach, University of Manchester, UK)
  • 12:00–12:30 Behavior Driven Formal Modelling (Colin Snook, University of Southampton, UK)
  • 12:30–13:00 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 The ASM Method Integrates Validation and Verification at Different Abstraction Levels (Egon Börger, University of Pisa, Italy)
  • 15:00–15:30 On the importance of scenario-based validation (Angelo Gargantini, University of Bergamo, Italy)
  • 15:30–16:00 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 DesignSpace for collaborative engineering (Alexander Egyed, JKU Linz, Austria)
  • 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 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)