Mediante una nueva metodología que permite adoptar y utilizar las herramientas de análisis de código fuente de manera eficiente en ámbitos de aplicación de menor criticidad. Se propone una nueva herramienta (Frama-C) y se validan sus capacidades en el sistema operativo Contiki, con la idea impulsar una etiqueta «Verified in Europe» para validar los productos de software con tecnologías como Frama-C.

El desarrollo de los métodos de verificación basados en la anotación del código fuente con distintas propiedades a cumplir y explicitando cuando no se cumplen. Éstos pueden ser estáticos o dinámicos dependiendo de si deben ejecutar el código o no, respectivamente. Los métodos de monitorización, por contra, modifican el programa de tal forma que en ejecución pueden detectar vulnerabilidades y ataques, e interrumpir su ejecución.