Thomas Huining Feng and Lynn Tao-Ning Wang and Wei Zheng and Sri Kanajan and Sanjit A. Seshia

EECS Department, University of California, Berkeley

Technical Report No. UCB/EECS-2006-117

September 25, 2006

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-117.pdf

Embedded systems are often assembled from black box components. System-level analyses, including verification and timing analysis, typically assume the system description, such as RTL or source code, as an input. There is therefore a need to automatically generate formal models of black box components to facilitate analysis.

We propose a new method to generate models of realtime embedded systems based on machine learning from execution traces, under a given hypothesis about the system's model of computation. Our technique is based on a novel formulation of the model generation problem as learning a dependency graph that indicates partial ordering between tasks. Tests based on an industry case study demonstrate that the learning algorithm can scale up and that the deduced system model accurately reflects dependencies between tasks in the original design. These dependencies help us formally prove properties of the system and also extract data dependencies that are not explicitly stated in the specifications of black box components.

---

BibTeX citation:

@techreport{Feng:EECS-2006-117,
    Author= {Feng, Thomas Huining and Wang, Lynn Tao-Ning and Zheng, Wei and Kanajan, Sri and Seshia, Sanjit A.},
    Title= {Automatic Model Generation for Black Box Real-Time Systems},
    Year= {2006},
    Month= {Sep},
    Url= {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-117.html},
    Number= {UCB/EECS-2006-117},
    Abstract= {Embedded systems are often assembled from black box components. System-level analyses, including verification and timing analysis, typically assume the system description, such as RTL or source code, as an input. There is therefore a need to automatically generate formal models of black box components to facilitate analysis.

We propose a new method to generate models of realtime embedded systems based on machine learning from execution traces, under a given hypothesis about the system's model of computation. Our technique is based on a novel formulation of the model generation problem as learning a dependency graph that indicates partial ordering between tasks. Tests based on an industry case study demonstrate that the learning algorithm can scale up and that the deduced system model accurately reflects dependencies between tasks in the original design. These dependencies help us formally prove properties of the system and also extract data dependencies that are not explicitly stated in the specifications of black box components.},
}

EndNote citation:

%0 Report
%A Feng, Thomas Huining 
%A Wang, Lynn Tao-Ning 
%A Zheng, Wei 
%A Kanajan, Sri 
%A Seshia, Sanjit A. 
%T Automatic Model Generation for Black Box Real-Time Systems
%I EECS Department, University of California, Berkeley
%D 2006
%8 September 25
%@ UCB/EECS-2006-117
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2006/EECS-2006-117.html
%F Feng:EECS-2006-117