Cyber-Physical Verification of Intermittently Powered Embedded Systems

Intermittently powered embedded systems are a foundational and growing component of the Internet of Things. It is essential to rigorously prove these systems' correctness because they arise both in safety-critical applications and applications where quality-of-service is essential to social good. Such proofs are challenging because they are simultaneously cyber-physical and time-sensitive: correctness is affected by physical properties that change with time. This article introduces a new general-purpose formal verification approach for cyber-physical properties of intermittent systems. We define a high-level modeling and specification language for intermittent systems, define its formal semantics, and prove that the language reduces to hybrid games, enabling the application of existing theorem-proving software. Cold storage for COVID vaccines serves as a running example; we provide a machine-checked proof that safe temperatures are maintained under suitable assumptions. The crux of our proof approach is to identify power and timing assumptions under which sufficient power is available to complete time-sensitive tasks. Orthogonal to approaches that prove new guarantees on power or timing, our work rigorously shows which power and timing assumptions are needed for cyber-physical correctness.