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 metadatas
Contributor : Delphine Demange <>
Submitted on : Tuesday, April 28, 2020 - 12:18:59 PM
Last modification on : Wednesday, September 30, 2020 - 8:45:13 AM



Gautier Berthou, Pierre-Evariste Dagand, Delphine Demange, Tanguy Risset, Rémi Oudin. 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