Reports

Here we list the publications and reports in which we present our work on each of the work packages laid out in the IVOIRE project proposal.

• WP1: Validation formalization
  • Validation Obligations: A Novel Approach to Check Compliance between Requirements and their Formal Specification
  • Classification of existing VOs & tools and Formalization of VOs semantics
  • Formalization of Advanced VOs semantics and VO Refinement
  • Validation by Abstraction and Refinement
• WP2: Validation refinement
  • Trace preservation in B and Event-B refinements
  • Trace Refinement in B and Event-B
  • Generating interactive documents for domain-specific validation of formal models
  • Generating Domain-Specific Interactive Validation Documents
  • Early and Systematic Validation of Formal Models
  • Validation-Driven Development
• WP3: VOs management framework
  • A VO manager implementation has been integrated into ProB2-UI and is further described in a journal article still under review.
  • Validation of Reinforcement Learning Agents and Safety Shields with ProB
  • Validation of Formal Models by Timed Probabilistic Simulation
  • Validation of Formal Models by Interactive Simulation
  • Model Checking B Models via High-Level Code Generation
• WP4: Case studies
  • Modeling and Analysis of a Safety-Critical Interactive System Through Validation Obligations
  • Validation of Reinforcement Learning Agents and Safety Shields with ProB
  • Application of Validation Obligations to Security Concerns