A Lesson on Verification of IoT Software with Frama-C
Allan Blanchard, Nikolaï Kosmatov, Frédéric Loulergue · 2018
This paper is a tutorial introduction to Frama- C, a framework for analysis and verification of C programs. We present value analysis, deductive verification and runtime verification of software using Frama-C and in particular its Eva, Wp, and E-Acsl plugins. These techniques are illustrated on examples coming from real-life verification case studies for different modules of Contiki, a lightweight operating system for the Internet of Things.