Article

Interactive presentation: Automatic model generation for black box real-time systems

Authors:

Sanjit A. SeshiaAuthors Info & Claims

DATE '07: Proceedings of the conference on Design, automation and test in Europe

Pages 930 - 935

Published: 16 April 2007 Publication History

Get Access

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 real-time 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.

References

[1]

OSEK OS version 2.2.3 specification, 2006.

Google Scholar

[2]

D. Angluin. Learning regular sets from queries and counterexamples. Information and Computation, 75:87--106, 1987.

Digital Library

Google Scholar

[3]

R. Bosch. CAN specification version 2.0, 1991.

Google Scholar

[4]

H. T. Feng, L. T.-N. Wang, W. Zheng, S. Kanajan, and S. A. Seshia. Automatic model generation for black box real-time systems. Technical Report UCB/EECS-2006-117, EECS Department, University of California, Berkeley, Sep 2006.

Google Scholar

[5]

J. G. Huselius, J. Andersson, H. Hansson, and S. Punnekkat. Automatic generation and validation of models of legacy software. In 12:th IEEE International Conference RTCSA, Sydney, Australia, August 2006.

Digital Library

Google Scholar

[6]

S. Kanajan, H. Zeng, C. Pinello, and A. Sangiovanni-Vincentelli. Exploring trade-off's between centralized versus decentralized automotive architectures using a virtual integration environment. In DATE'06, March 2006.

Digital Library

Google Scholar

[7]

T. A. Lau, P. Domingos, and D. S. Weld. Learning programs from traces using version space algebra. In International Conference on Knowledge Capture (K-CAP), pages 36--43, Banff, Alberta, Canada, 2003.

Digital Library

Google Scholar

[8]

E. A. Lee and A. L. Sangiovanni-Vincentelli. A denotational framework for comparing models of computation. IEEE Transactions on CAD, 17(12), 1998.

Digital Library

Google Scholar

[9]

T. M. Mitchell. Generalization as search. Artificial Intelligence, 18:203--226, 1982.

Crossref

Google Scholar

[10]

M. D. Natale, P. Giusto, S. Kanajan, C. Pinello, and P. Popp. Architecture exploration for time-critical and cost-sensitive distributed systems. In Proceedings of the SAE Conference, 2007.

Crossref

Google Scholar

[11]

P. Pop. Analysis and Synthesis of Communication-Intensive Heterogeneous Real-Time Systems. PhD thesis, Dept. of Computer and Information Science, Linköping University, Sweden, 2003.

Google Scholar

[12]

R. L. Rivest and R. E. Schapire. Diversity-based inference of finite automata. J. ACM, 41(3):555--589, 1994.

Digital Library

Google Scholar

[13]

K. Tindell and J. Clark. Holistic schedulability analysis for distributed hard real-time systems. Microprocessing and Microprogramming - Euromicro Journal (Special Issue on Parallel Embedded Real-Time Systems), 40:117--134, 1994.

Digital Library

Google Scholar

Cited By

View all

Neves FVilaça RPereira J(2021)Detailed black-box monitoring of distributed systemsACM SIGAPP Applied Computing Review10.1145/3477133.347713521:1(24-36)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1145/3477133.3477135
de Oliveira Neto FFeldt RTorkar RMachado PPaige RHarman MWilliams J(2013)Searching for models to evaluate software technologyProceedings of the 1st International Workshop on Combining Modelling and Search-Based Software Engineering10.5555/2662572.2662578(12-15)Online publication date: 19-May-2013
https://dl.acm.org/doi/10.5555/2662572.2662578
Dominka SBroecker ESchiller FJefferson TFowler JIngalls R(2008)Automated execution of simulation studies demonstrated via a simulation of a carProceedings of the 40th Conference on Winter Simulation10.5555/1516744.1517254(2916-2924)Online publication date: 7-Dec-2008
https://dl.acm.org/doi/10.5555/1516744.1517254

Recommendations

A Cloud-Based Black-Box Solar Predictor for Smart Homes
Special Issue on Smart Homes, Buildings and Infrastructures

The popularity of rooftop solar for homes is rapidly growing. However, accurately forecasting solar generation is critical to fully exploiting the benefits of locally generated solar energy. In this article, we present two machine-learning techniques to ...
Learning-based black box checking for k-safety hyperproperties
Abstract
The L ∗ algorithm proposed by Angluin is a standard approach to automata learning of unknown systems that generate regular languages. Black box checking (BBC) based on the L ∗ algorithm is a promising formal verification of unknown systems. On ...
Graphical abstract

Display Omitted
Highlights
- Automata learning based black box checking algorithm for k-safety hyperproperties.
- Generation of k-bad prefix automata with L ∗ algorithm.
- Demonstration of black box checking of mobile robot path planning.
Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

Currently available application frameworks that target the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal ...

Comments

Information & Contributors

Information

Published In

DATE '07: Proceedings of the conference on Design, automation and test in Europe

April 2007

1741 pages

ISBN:9783981080124

General Chair:
Rudy Lauwereins
IMEC and KULeuven, Belgium
,
Program Chair:
Jan Madsen
DTU, Denmark

Publisher

EDA Consortium

San Jose, CA, United States

Publication History

Published: 16 April 2007

Check for updates

Qualifiers

Article

Conference

DATE07

Sponsor:

EDAA
SIGDA
The Russian Academy of Sciences

DATE07: Design, Automation and Test in Europe

April 16 - 20, 2007

Nice, France

Acceptance Rates

Overall Acceptance Rate 518 of 1,794 submissions, 29%

Upcoming Conference

DATE '25

Sponsor:
sigda

Design, Automation and Test in Europe

March 31 - April 2, 2025

Lyon , France

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

3
Total Citations
View Citations
143
Total Downloads

Downloads (Last 12 months)1
Downloads (Last 6 weeks)0

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

View all

Neves FVilaça RPereira J(2021)Detailed black-box monitoring of distributed systemsACM SIGAPP Applied Computing Review10.1145/3477133.347713521:1(24-36)Online publication date: 20-Jul-2021
https://dl.acm.org/doi/10.1145/3477133.3477135
de Oliveira Neto FFeldt RTorkar RMachado PPaige RHarman MWilliams J(2013)Searching for models to evaluate software technologyProceedings of the 1st International Workshop on Combining Modelling and Search-Based Software Engineering10.5555/2662572.2662578(12-15)Online publication date: 19-May-2013
https://dl.acm.org/doi/10.5555/2662572.2662578
Dominka SBroecker ESchiller FJefferson TFowler JIngalls R(2008)Automated execution of simulation studies demonstrated via a simulation of a carProceedings of the 40th Conference on Winter Simulation10.5555/1516744.1517254(2916-2924)Online publication date: 7-Dec-2008
https://dl.acm.org/doi/10.5555/1516744.1517254

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Abstract

References

Cited By

Recommendations

A Cloud-Based Black-Box Solar Predictor for Smart Homes

Learning-based black box checking for k-safety hyperproperties

Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

Comments

Information

Published In

Sponsors

Publisher

Publication History

Check for updates

Qualifiers

Conference

Acceptance Rates

Upcoming Conference

Contributors

Other Metrics

Bibliometrics

Article Metrics

Other Metrics

Citations

Cited By

Login options

Full Access

View options

PDF

eReader

Share

Share this Publication link

Share on social media

Affiliations