Towards verifiable deeply embedded systems

Abstract

An important class of deeply embedded systems (DES) involves interlocking cyber-physical control loops, each with its own dynamics and correctness constraints. For instance, in medical systems which monitor a patient's vital signs and control drug infusion rates, multiple sensing and control systems may be implicitly coupled. These systems present new challenges for control theory, scheduling and verification. What is needed are platforms capable of precise monitoring and enforcement of diverse execution constraints, and techniques to verify system correctness.