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 SoftwareWe have recently applied a combination of statistical learning and verification techniques (based on SAT and SMT) to estimate the execution time of tasks.
Autonomic Reactive SystemsIs 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.
Model GenerationAnalyzing 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.
SupportThis 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.