Validation assistance (by simulation)
Formal methods for the verification of embedded systems

If formal methods are applied in processes requiring the highest levels of guarantees, they cannot always be successful, due to the combinatorial explosion or over-approximations that are too crude to apply in order to reach a conclusion. (Functional) test methods are still widely used. Being non-exhaustive, they pose the problem of selecting, from an infinite set of stimulus sequences to be applied, a finite, extremely reduced subset, enabling the system to be placed in hard-to-reach configurations that have been identified as particularly sensitive. Formal methods can be used to help select these relevant sequences, as well as to build observers that analyze properties of the system specification during runtime.