Hi-Lite Progress

Schedule for Deliveries (AdaCore only for now)

• 2010-12-25: ALFA/E-ACSL description + initial plan for translation in Ada/C (for execution) and SPARK/Why (for formal verification)
• 2010-12-25: simulation of the final product for the Web
• 2011-03-31: support for Ada 2012 in GNAT compiler
• 2011-05-01: verification toolkit v0.1 with complete support for unit testing (based on AUnit and ideas from QuickCheck adapted to Ada 2012 contracts)
• 2012-05-01: verification toolkit v0.2 with complete support for unit testing and unit proof
• 2013-05-01: verification toolkit v1.0

WP1: Management and Dissemination

• Project Proposal (2009-11-26)
• initial technical project description (in French)
• annex B: Examples of Possible Industrial Use of Hi-Lite (in French)
• annex C: FLOSS, COTS, and Safety: A Business Perspective
• Kickoff (2010-05-04)
  • slides of the public presentation (in French)

WP2: Specifications

• First meeting (2010-07-13)
  • initial proposal for ALFA (by AdaCore)
  • initial proposal for E-ACSL (by CEA LIST)
  • wish-list, examples and discussion of ECSS-E-40 (by Astrium)
  • presentation of MyCCM and wish-list (by Thales)

WP3: Languages

WP4: Translators

WP5: Analysis and Testing Tools

WP6: Libraries and User Interfaces