Ghosts for Lists: from Axiomatic to Executable Specifications

Abstract : Internet of Things (IoT) applications are becoming increasingly critical and require formal verification. Our recent work presented formal verification of the linked list module of Contiki, an OS for IoT. It relies on a parallel view of a linked list via a companion ghost array and uses an inductive predicate to link both views. In this work, a few interactively proved lemmas allow for the automatic verification of the list functions specifications, expressed in the acsl specification language and proved with the Frama-C/Wp tool. In a broader verification context, especially as long as the whole system is not yet formally verified, it would be very useful to use runtime verification , in particular, to test client modules that use the list module. It is not possible with the current specifications, which include an inductive predicate and axiomatically defined functions. In this early-idea paper we show how to define a provably equivalent non-inductive predicate and a provably equivalent non-axiomatic function that belong to the executable subset e-acsl of acsl and can be transformed into executable C code. Finally, we propose an extension of Frama-C to handle both axiomatic specifications for deductive verification and executable specifications for runtime verification.
Type de document :
Communication dans un congrès
TAP 2018 - 12th International Conference on Tests and Proofs, Jun 2018, Toulouse, France
Liste complète des métadonnées

Littérature citée [11 références]  Voir  Masquer  Télécharger
Contributeur : Allan Blanchard <>
Soumis le : lundi 11 juin 2018 - 09:05:07
Dernière modification le : lundi 24 septembre 2018 - 11:34:02
Document(s) archivé(s) le : jeudi 13 septembre 2018 - 00:06:09


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01811922, version 1



Frédéric Loulergue, Allan Blanchard, Nikolai Kosmatov. Ghosts for Lists: from Axiomatic to Executable Specifications. TAP 2018 - 12th International Conference on Tests and Proofs, Jun 2018, Toulouse, France. 〈hal-01811922〉



Consultations de la notice


Téléchargements de fichiers