>home/research/

Embedded Systems

Model Based Design and Verification of Embedded Systems
PI: Radu Grosu 

Computer aided verification (CAV) and embedded software design automation (ESDA) emerge from academia and industry respectively as two promising approaches to developing the high-confidence software demanded by embedded-system applications, including those found in the telecommunications, aerospace/military, medical-device, and automotive industries. CAV and ESDA advocate the same methodology for system design:
1) define the requirements
2) construct a model and
3) analyze the model with respect to the requirements.

The difference is essentially that:
1) CAV uses more sophisticated requirements
2) ESDA uses more sophisticated models and
3) CAV performs a more sophisticated analysis. While ESDA analysis reduces to manual, pointwise simulation of the model, CAV analysis is automatic and exhaustive. This is made possible by a mathematical formulation of the requirements, models and analysis problem that is far beyond the precision currently supported by ESDA.

The goal of this research is to:
1) push the limits of CAV to capture and analyze ESDA models
2) increase the confidence in ESDA by applying CAV techniques 
(NSF)