A Lesson on Verification of IoT Software with Frama-C

Allan Blanchard (1) , Nikolai Kosmatov (2) , Frédéric Loulergue (3, 4)

1 FUN - Self-organizing Future Ubiquitous Network
2 LSL - Laboratoire Sûreté des Logiciels
3 Northern Arizona University [Flagstaff]
4 LIFO - Laboratoire d'Informatique Fondamentale d'Orléans

This paper is a tutorial introduction to Frama-C, a framework for the analysis and verification of sequential C programs, and in particular its EVA, WP, and E-ACSL plugins. The examples are drawn from Contiki, a lightweight operating system for the Internet of Things.

Domaines: Langage de programmation [cs.PL]

Allan Blanchard, Nikolai Kosmatov, Frédéric Loulergue. A Lesson on Verification of IoT Software with Frama-C. 2018 International Conference on High Performance Computing & Simulation (HPCS), Jul 2018, Orleans, France. pp.21-30, ⟨10.1109/HPCS.2018.00018⟩. ⟨hal-02317078⟩