Final report of the DAEDALUS project

on the Validation of critical software by static analysis and abstract testing

DAEDALUS is the shared-cost research and technology development (RTD) project IST-1999-20527 of the european IST Programme of the Fifth Framework Programme (FP5) on the « validation of software components embedded in future generation critical concurrent systems by exhaustive semantic-based static analysis and abstract testing methods based on abstract interpretation ».

Present software verification methods (such as testing, simulation, code review and formal methods including deductive methods or model checking) do not scale up for software of several hundred thousand lines, in particular for essential properties in embedded critical software such as absence of runtime errors, worst-case execution time, data races, precision of floating-point computations, etc. The DAEDALUS project has explored static analysis methods based on abstract interpretation. The approach has been shown to be effective on software provided by Airbus France.

DAEDALUS basic research main results
Preliminary exploration work has also been done on mid-term and long-term problems related to the analysis of future generation embedded software (Yet unpublished technical reports are marked “TR”).

DAEDALUS participants
  • Coordinators:
  • Participants: