Robust Embedded Systems

Embedded systems are those that integrate computation with physical dynamics. Examples of such systems include automotive controllers, sensor nodes, medical devices, and autonomous robots. Our reliance on such systems is significant and growing. It is necessary to make these systems robust to failures and to devise tools to evaluate their behavior in uncertain and adversarial operating environments.

In this project, we are developing algorithmic techniques for formal verification and statistical learning and use them for the analysis, diagnosis, and repair of embedded systems.

A few sample papers are given below. For a more recent list of related publications, please follow this link.

 Quantitative Analysis of Software

We have recently applied a combination of statistical learning and verification techniques (based on SAT and SMT) to estimate the execution time of tasks.
Game-Theoretic Timing Analysis
Sanjit A. Seshia and Alexander Rakhlin
In IEEE/ACM Conference on Computer-Aided Design (ICCAD), November 2008.


 Autonomic Reactive Systems

Is it possible to automatically diagnose and recover systems from failures arising from design errors and program bugs? Systems with such a capability are variously labeled as "autonomic", "fault-tolerant", or "self-repairing" systems.

In some exploratory work, we applied online learning to this question and found that it can provide a useful basis for an algorithmic approach to self-repair.

Autonomic Reactive Systems via Online Learning
Sanjit A. Seshia.
In Proc. IEEE International Conference on Autonomic Computing (ICAC), June 2007.


 Model Generation

Analyzing system dependability requires having descriptions of all system components. However, in many cases, some components are unspecified, untrusted, or unknown; e.g., untrusted third-party black-box components. In such cases, one can employ learning to infer models from sample executions.

Our current interest is in inferring models of timed circuits and systems. Some results have been obtained for a class of real-time systems used in automotive applications.

Automatic Model Generation for Black Box Real-Time Systems
Huining Thomas Feng, Lynn Tao-Ning Wang, Wei Zheng, Sri Kanajan and Sanjit A. Seshia.
In Proc. Design Automation and Test in Europe (DATE), April 2007, pages 930-935.



This project receives generous support from the National Science Foundation (NSF CAREER grant CNS-0644436), the SRC FCRP Gigascale Systems Research Center, Microsoft Research, and an equipment grant from Intel.

  Sanjit A. Seshia, last updated August 2010.