research-article

Verification of temporal properties in automotive embedded software

Authors:

Djones Lettnin,

Pradeep K. Nalla,

Wolfgang Rosenstiel,

Tobias Kirsten,

Volker Schönknecht,

Stephan ReitemeyerAuthors Info & Claims

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

Pages 164 - 169

https://doi.org/10.1145/1403375.1403417

Published: 10 March 2008 Publication History

Abstract

The amount of software in embedded systems has increased significantly over the last years and, therefore, the verification of embedded software is of fundamental importance. One of the main problems in embedded software is to verify variables and functions based on temporal properties. Formal property verification using model checker often suffers from the state space explosion problem when a large software design is considered. In this paper, we propose two new approaches to integrate assertions in the verification of embedded software using simulation-based verification. Firstly, we extended a SystemC hardware temporal checker with interfaces in order to monitor the embedded software variables and functions that are stored in a microprocessor memory model. Secondly, we derived a SystemC model from the original C program in order to integrate directly with the SystemC temporal checker. We performed a case study on an embedded software from automotive industry which is responsible for controlling read and write requests to a non-volatile memory.

References

[1]

Accellera. Property Specification Language (PSL), Version 1.1, June 2004.

[2]

J. Andrews. Co-Verification of Hardware and Software for Arm Soc Design. Newnes, 2005.

[3]

D. Beyer, A. J. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar. The BLAST query language for software verification. In Proceedings of the 11th international Static Analysis Symposium, pages 26--28. LNCS 3148, Pages 2--18, 2004, 2004.

[4]

CMU. CBMC: Bounded Model Checking for ANSI-C. http://www.cs.cmu.edu/~modelcheck/cbmc/.

[5]

T. Grötker, S. Liao, G. Martin, and S. Swan. System design with SystemC. Kluwer Academic Publishers, 2002.

Digital Library

[6]

T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In 10th International Workshop on Model Checking of Software (SPIN), volume 2648 of Lecture Notes in Computer Science, pages 235--239, 2003.

Digital Library

[7]

C. N. Ip and S. Swan. A Tutorial Introduction on the New SystemC Verification Standard. In White Paper, 2003.

[8]

F. Ivanicic, I. Shlyakhter, A. Gupta, and M. K. Ganai. Model checking C programs using F-SOFT. In ICCD '05: Proceedings of the 2005 International Conference on Computer Design, pages 297--308, Washington, DC, USA, 2005. IEEE Computer Society.

Digital Library

[9]

C. N. C. Jr. and H. D. Foster. Assertion-based verification. In R. Drechsler, editor, Advanced Formal Verification, pages 167--204. Kluwer Academic Publishers, Dordrecht, The Netherlands, 2004.

[10]

Y. Nakamura, K. Hosokawa, I. Kuroda, K. Yoshikawa, and T. Yoshimura. A Fast Hardware/Software Co-Verification Method for System-On-a-Chip by Using a C/C++ Simulator and FPGA Emulator with Shared Register Communication. In Design Automation Conference (DAC), pages 299--304, Los Alamitos, CA, USA, 2004. IEEE Computer Society.

Digital Library

[11]

NEC. NEC Electronics (Europe) GmbH. http://www.eu.necel.com/.

[12]

G. Post, P. Venkataraghavan, T. Ray, and D. R. Seetharaman. A SystemC-based verification methodology for complex wireless software IP. In DATE '04:Design, Automation and Test in Europe Conference and Exhibition, 2004, volume 1, pages 544--550. IEEE Computer Society, 2004.

Digital Library

[13]

J. Ruf, D. W. Hoffmann, T. Kropf, and W. Rosenstiel. Simulation-guided property checking based on a multi-valued AR-automata. In W. Nebel and A. Jerraya, editors, Design, Automation and Test in Europe 2001, pages 742--748. IEEE Press, 2001.

Digital Library

[14]

SatAbs. SATABS - predicate abstraction with SAT for ANSI-C. http://www.verify.ethz.ch/satabs/.

[15]

B. Schlich and S. Kowalewski. Model checking C source code for embedded systems. In IEEE/NASA Workshop on Leveraging Applications of Formal Methods, Verification, and Validation (IEEE/NASA ISoLA 2005), pages 65--77. NASA, 2005.

[16]

SLAM. Software model checking with SLAM. http://research.microsoft.com/SLAM/.

[17]

M. Winterholer. Transaction-based Hardware Software Co-verification. In FDL '06: Proceedings of the conference on Forum on Specification & Design Languages, 2006.

Cited By

Chung YKim DChoi Y(2017)Modeling OSEK/VDX OS Requirements in C2017 24th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2017.46(398-407)Online publication date: Dec-2017
https://doi.org/10.1109/APSEC.2017.46
Pravadelli GQuaglia DVinco SFummi F(2017)Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design FrameworkHandbook of Hardware/Software Codesign10.1007/978-94-017-7358-4_23-2(1-38)Online publication date: 14-Apr-2017
https://doi.org/10.1007/978-94-017-7358-4_23-2
Pravadelli GQuaglia DVinco SFummi F(2017)Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design FrameworkHandbook of Hardware/Software Codesign10.1007/978-94-017-7267-9_23(683-720)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-94-017-7267-9_23
Show More Cited By

Index Terms

Recommendations

Semiformal verification of temporal properties in automotive hardware dependent software
DATE '09: Proceedings of the Conference on Design, Automation and Test in Europe

The verification of embedded software has become an important subject over the last years. This work presents a new semiformal verification approach called SofTPaDS. It combines assertion-based and symbolic simulation approaches for the verification of ...
Embedded software verification: challenges and solutions
ICCAD '08: Proceedings of the 2008 IEEE/ACM International Conference on Computer-Aided Design

Embedded software are becoming more and more pervasive in our lives, and many application domains have very high reliability requirements. Ensuring high software quality while still maintaining software productivity is a challenging task. In order to ...
Scalable and Optimized Hybrid Verification of Embedded Software

The verification of embedded software has become an important subject over the last years. However, neither standalone verification approaches, like simulation-based/formal verification, nor state-of-the-art semiformal verification approaches are able ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

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

March 2008

1575 pages

ISBN:9783981080131

DOI:10.1145/1403375

General Chair:
Donatella Sciuto
Politecnico di Milano, Italy

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

The EDA Consortium
EDAA: European Design Automation Association
ECSI
SIGDA: ACM Special Interest Group on Design Automation
The IEEE Computer Society TTTC
IEEE Council on Electronic Design Automation (CEDA)
The Russian Academy of Sciences: The Russian Academy of Sciences

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 March 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Research-article

Conference

DATE '08

Sponsor:

EDAA
SIGDA
The Russian Academy of Sciences

DATE '08: Design, Automation and Test in Europe

March 10 - 14, 2008

Munich, Germany

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

10
Total Citations
View Citations
293
Total Downloads

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

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Chung YKim DChoi Y(2017)Modeling OSEK/VDX OS Requirements in C2017 24th Asia-Pacific Software Engineering Conference (APSEC)10.1109/APSEC.2017.46(398-407)Online publication date: Dec-2017
https://doi.org/10.1109/APSEC.2017.46
Pravadelli GQuaglia DVinco SFummi F(2017)Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design FrameworkHandbook of Hardware/Software Codesign10.1007/978-94-017-7358-4_23-2(1-38)Online publication date: 14-Apr-2017
https://doi.org/10.1007/978-94-017-7358-4_23-2
Pravadelli GQuaglia DVinco SFummi F(2017)Semiformal Assertion-Based Verification of Hardware/Software Systems in a Model-Driven Design FrameworkHandbook of Hardware/Software Codesign10.1007/978-94-017-7267-9_23(683-720)Online publication date: 27-Sep-2017
https://doi.org/10.1007/978-94-017-7267-9_23
Lettnin DWinterholer M(2017)An Overview About Debugging and Verification Techniques for Embedded SoftwareEmbedded Software Verification and Debugging10.1007/978-1-4614-2266-2_1(1-18)Online publication date: 19-Apr-2017
https://doi.org/10.1007/978-1-4614-2266-2_1
Behrend JLettnin DGrünhage ARuf JKropf TRosenstiel W(2015)Scalable and Optimized Hybrid Verification of Embedded SoftwareJournal of Electronic Testing: Theory and Applications10.1007/s10836-015-5518-431:2(151-166)Online publication date: 1-Apr-2015
https://dl.acm.org/doi/10.1007/s10836-015-5518-4
Mukherjee RMukherjee SDasgupta PGhosal SShroff GChandra SNagappan N(2013)Model checking of global power management strategies in software with temporal logic propertiesProceedings of the 6th India Software Engineering Conference10.1145/2442754.2442759(29-34)Online publication date: 21-Feb-2013
https://dl.acm.org/doi/10.1145/2442754.2442759
Di Guglielmo GDi Guglielmo LFummi FPravadelli GRosenstiel WMacii E(2012)Enabling dynamic assertion-based verification of embedded software through model-driven designProceedings of the Conference on Design, Automation and Test in Europe10.5555/2492708.2492761(212-217)Online publication date: 12-Mar-2012
https://dl.acm.org/doi/10.5555/2492708.2492761
Braun ABringmann OLettnin DRosenstiel WDe Micheli GAl-Hashimi BMueller WMacii E(2010)Simulation-based verification of the MOST NetInterface specification revision 3.0Proceedings of the Conference on Design, Automation and Test in Europe10.5555/1870926.1871053(538-543)Online publication date: 8-Mar-2010
https://dl.acm.org/doi/10.5555/1870926.1871053
Lettnin DNalla PBehrend JRuf JGerlach JKropf TRosenstiel WSchönknecht VReitemeyer SBenini LDe Micheli GAl-Hashimi BMueller W(2009)Semiformal verification of temporal properties in automotive hardware dependent softwareProceedings of the Conference on Design, Automation and Test in Europe10.5555/1874620.1874912(1214-1217)Online publication date: 20-Apr-2009
https://dl.acm.org/doi/10.5555/1874620.1874912
Lettnin DNalla PBehrend JRuf JGerlach JKropf TRosenstiel WSchonknecht VReitemeyer S(2009)Semiformal verification of temporal properties in automotive hardware dependent software2009 Design, Automation & Test in Europe Conference & Exhibition10.1109/DATE.2009.5090847(1214-1217)Online publication date: Apr-2009
https://doi.org/10.1109/DATE.2009.5090847

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.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents