Skip to Main content Skip to Navigation
Conference papers

Intermittent Computing with Peripherals, Formally Verified

Abstract : Transiently-powered systems featuring non-volatile memory as well as external peripherals enable the development of new low-power sensor applications. However, as programmers, we are ill-equipped to reason about systems where power failures are the norm rather than the exception. A first challenge consists in being able to capture all the volatile state of the application -- external peripherals included -- to ensure progress. A second, more fundamental, challenge consists in specifying how power failures may interact with peripheral operations. In this paper, we propose a formal specification of intermittent computing with peripherals, an axiomatic model of interrupt-based checkpointing as well as its proof of correctness, machine-checked in the Coq proof assistant. We also illustrate our model with several systems proposed in the literature.
Document type :
Conference papers
Complete list of metadata
Contributor : Delphine Demange Connect in order to contact the contributor
Submitted on : Saturday, December 12, 2020 - 1:01:20 AM
Last modification on : Wednesday, September 28, 2022 - 3:06:06 PM
Long-term archiving on: : Saturday, March 13, 2021 - 6:14:47 PM


Files produced by the author(s)



Gautier Berthou, Pierre-Evariste Dagand, Delphine Demange, Rémi Oudin, Tanguy Risset. Intermittent Computing with Peripherals, Formally Verified. LCTES '20 - 21st ACM SIGPLAN/SIGBED Conference on Languages, Compilers, and Tools for Embedded Systems, Jun 2020, London / Virtual, United Kingdom. pp.85-96, ⟨10.1145/3372799.3394365⟩. ⟨hal-02556878⟩



Record views


Files downloads