research-article

Rigorous model-based design & verification flow for in-vehicle software

Authors:

A. GadkariAuthors Info & Claims

DAC '11: Proceedings of the 48th Design Automation Conference

Pages 13 - 16

https://doi.org/10.1145/2024724.2024728

Published: 05 June 2011 Publication History

Abstract

The development of in-vehicle software, often controlling safety-critical functions related to braking, steering and transmission systems, requires rigorous techniques to ensure high-integrity and reliability requirements. Formal models of requirements and design artifacts based on state-transition systems and other formalisms serve as a means to apply rigorous analysis and verification techniques at every stage in the development process. We present here one such formal analysis and verification flow, developed at General Motors R&D, provide an overview of methods for automatic test generation based on mathematical modeling and discuss the future directions for research.

References

[1]

Aditya Kanade, Rajeev Alur, Franjo Ivancic, S. Ramesh, Sriram Sankaranarayanan, and K. C. Shashidhar. Generating and analyzing symbolic traces of simulink/stateflow models. In Ahmed Bouajjani and Oded Maler, editors, CAV, volume 5643 of Lecture Notes in Computer Science, pages 430--445. Springer, 2009.

Digital Library

[2]

AGEDIS consortium homepage. http://www.agedis.de.

[3]

Ambar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh, Swarup Mohalik, and K. C. Shashidhar. AutoMOTGen: Automatic model oriented test generator for embedded control systems. In Aarti Gupta and Sharad Malik, editors, CAV, volume 5123 of Lecture Notes in Computer Science, pages 204--208. Springer, 2008.

Digital Library

[4]

Angelo Gargantini and Constance L. Heitmeyer. Using model checking to generate tests from requirements specifications. In ESEC/SIGSOFT FSE, pages 146--162, 1999.

Digital Library

[5]

BEACON Tester, Applied Dynamics International, http://www.adi.com/products_be_bss_te.htm.

[6]

Bernhard K. Aichernig, Harald Brandl, and Franz Wotawa. Conformance testing of hybrid systems with qualitative reasoning models. Electr. Notes Theor. Comput. Sci., 253(2):53--69, 2009.

Digital Library

[7]

Boehm, B. W. (1981). Software Engineering Economics. Englewood Cliffs, NJ: Prentice-Hall.

Digital Library

[8]

E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, Cambridge, MA, 1999.

Digital Library

[9]

Ghezzi, C. & Nuseibeh, B. (1998). Guest Editorial -- Managing Inconsistency in Software Development. Transactions on Software Engineering, 24(11): 906--907.

Digital Library

[10]

Glenford J. Myers. The Art of Software Testing, 2nd edition. Wiley. 2004.

Digital Library

[11]

Gr'egoire Hamon, Leonardo deMoura, and John Rushby. Generating efficient test sets with a model checker. In 2nd International Conference on Software Engineering and Formal Methods, pages 261--270, Beijing, China, September 2004. IEEE Computer Society.

Digital Library

[12]

Heitmeyer, C. L., Jeffords, R. D. & Labaw, B. G. (1996). Automated Consistency Checking of Requirements Specifications. IEEE Transactions on Software Engineering and Methodology, 5(3): 231--261.

Digital Library

[13]

IBM Rational DOORS. http://www-01.ibm.com/software/awdtools/doors/productline/

[14]

Jackson, M. (1995). Software Requirements and Specifications: A Lexicon of Practice, Principles and Prejudices. Addison Wesley.

Digital Library

[15]

Manfred Broy, Bengt Jonsson, Joost-Pieter Katoen, Martin Leucker, and Alexander Pretschner, editors. Model-Based Testing of Reactive Systems, Advanced Lectures {The volume is the outcome of a research seminar that was held in Schloss Dagstuhl in January 2004}, volume 3472 of Lecture Notes in Computer Science. Springer, 2005.

Digital Library

[16]

Manfred Broy. Challenges in automotive software engineering. 28th International Conference on Software Engineering (ICSE'06), 2006.

Digital Library

[17]

Manoranjan Satpathy, Anand Yeolekar, and S. Ramesh. Randomized directed testing (redirect) for simulink/stateflow models. In de Alfaro and Palsberg {10}, pages 217--226.

Digital Library

[18]

M. Satpathy, Ramesh S. Formal Foundation to Systematic Development of Simulink/Stateflow models, Proc. of the Dagstuhl Seminar on Refinement based methods for the construction of dependable systems, 2009.

[19]

Mark Utting and Bruno Legeard. Practical Model-Based Testing: A Tools Approach. Morgan-Kaufmann, 2006.

Digital Library

[20]

Object Management Group. http://www.uml.org

[21]

Paul Ammann, Paul E. Black, and William Majurski. Using model checking to generate tests from specifications. In ICFEM, page 46, 1998.

Digital Library

[22]

Reactis, Reactive Systems, Inc., http://www.reactive-systems.com.

[23]

Saaltink, M. (1997). The Z/EVES System. 19th International Conference on the Z Formal Method (ZUM), Reading, UK, April 1997, LNCS 1212, pp. 72--88.

Digital Library

[24]

Safety Test Builder, chiastek inc., http://www.chiastek.com/products/stb.html.

[25]

Sethu Ramesh, P. Vignesh V. Ganesan, Gurulingesh Raravi: A Formal Framework for the Correct-by-construction and Verification of Distributed Time Triggered Systems. SIES 2007: 63--70.

[26]

Swarup Mohalik, A. C. Rajeev, Manoj G. Dixit, S. Ramesh, P. Vijay Suman, Paritosh K. Pandya, Shengbing Jiang: Model checking based analysis of end-to-end latency in embedded, realtime systems with clock drifts. DAC 2008: 296--299.

Digital Library

[27]

The B Method. http://www.b-core.com/ONLINEDOC/BMethod.html

[28]

The MathWorks, Inc. http://www.mathworks.com.

[29]

Zave, P. (1997). Classification of Research Efforts in Requirements Engineering. ACM Computing Surveys, 29(4): 315--321.

Digital Library

Cited By

de Oliveira JKreutz M(2024)The Blind Spots of Two-Factor Authentication ToolsProceedings of the Third International Conference on Innovations in Computing Research (ICR’24)10.1007/978-3-031-65522-7_50(580-592)Online publication date: 1-Aug-2024
https://doi.org/10.1007/978-3-031-65522-7_50
Wan JCanedo AAl Faruque M(2015)Cyber–Physical Codesign at the Functional Level for Multidomain Automotive SystemsIEEE Systems Journal10.1109/JSYST.2015.2472495(1-11)Online publication date: 2015
https://doi.org/10.1109/JSYST.2015.2472495

Recommendations

Formal specification at model-level of model-driven engineering using modelling techniques

Nowadays Model-Driven Engineering (MDE) is gaining more popularity due to high-level development leading to a faster generation of executable code, which reduces manual intervention. Verification is crucial at different levels of model-based development. ...
Refinement-Based Verification of Interactive Real-Time Systems

Formal specification provides a system description that is much more precise than the natural language one and it can help to solve a lot of specification problems. But even a formal specification of a system can contain mistakes or can disagree with ...
The echo approach to formal verification
ICSE '06: Proceedings of the 28th international conference on Software engineering

In this research abstract, we propose Echo: a general formal verification approach that combines theorem proving, model checking, and code-level tools to show an implementation's compliance with its formal specification. We believe that this approach is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '11: Proceedings of the 48th Design Automation Conference

June 2011

1055 pages

ISBN:9781450306362

DOI:10.1145/2024724

General Chair:
Leon Stok
IBM Corp., Hopewell Jct., NY
,
Program Chairs:
Nikil Dutt
Univ. of California, Irvine, CA
,
Soha Hassoun
Tufts Univ., Medford, MA

Copyright © 2011 Authors.

Sponsors

EDAC: Electronic Design Automation Consortium
SIGDA: ACM Special Interest Group on Design Automation
IEEE Council on Electronic Design Automation (CEDA)

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 05 June 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

DAC '11

Sponsor:

EDAC
SIGDA

DAC '11: The 48th Annual Design Automation Conference 2011

June 5 - 10, 2011

California, San Diego

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
237
Total Downloads

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

Reflects downloads up to 26 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

de Oliveira JKreutz M(2024)The Blind Spots of Two-Factor Authentication ToolsProceedings of the Third International Conference on Innovations in Computing Research (ICR’24)10.1007/978-3-031-65522-7_50(580-592)Online publication date: 1-Aug-2024
https://doi.org/10.1007/978-3-031-65522-7_50
Wan JCanedo AAl Faruque M(2015)Cyber–Physical Codesign at the Functional Level for Multidomain Automotive SystemsIEEE Systems Journal10.1109/JSYST.2015.2472495(1-11)Online publication date: 2015
https://doi.org/10.1109/JSYST.2015.2472495

View Options

Get Access

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.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents