Robust Reactive Systems

Reactive systems are those that maintain an ongoing interaction with their environment at a speed dictated by the latter. Examples of such systems include microprocessors, web servers, network routers, sensor nodes, and autonomous robots. Our reliance on such systems is significant and growing, and it is necessary to make them error resilient.

This project investigates the use of formal, algorithmic techniques for verification and learning in the construction of error-resilient systems at low overhead.

There are currently a few different research tracks, described below.

 Verification-Guided Error Resilience

We are investigating the use of formal and semi-formal verification in the construction of systems resilient to device failures including those arising from soft errors, aging, environmental and parameter variations, and aggressive deployment of techniques to reduce resource consumption (e.g., power). Such resilience must be achieved at low overheads on power, performance, area, etc. Defining "resilience" also requires a good specification of system functionality.

As a first step, we are investigating using formal analysis in the construction of sequential digital circuits resilient to soft errors.

People

Wenchao Li
Sanjit A. Seshia
Orna Kupferman (Hebrew University)
Subhasish Mitra (Stanford)

Publications

Verification-Guided Soft Error Resilience
Sanjit A. Seshia, Wenchao Li, and Subhasish Mitra.
In Proc. Design Automation and Test in Europe (DATE), April 2007, pages 1442-1447.

 

 Autonomic Reactive Systems

We are adapting algorithmic techniques for verification and learning to automatically diagnose and recover systems from failures arising from design errors and program bugs. The terms "autonomic", "robust", "fault-tolerant", or "self-repairing" are variously used to describe systems with such capability. This project is especially focussed on embedded and networked systems.

Our initial results indicate that for a certain class of reactive systems, online learning provides a useful basis for an algorithmic approach to self-repair.

Publications

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.

Publications

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.

 

 Support

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 2007.