More Web Proxy on the site http://driver.im/

research-article

Where formal verification can help in functional safety analysis

Authors:

Alessandro Bernardini,

Wolfgang Ecker,

Ulf SchlichtmannAuthors Info & Claims

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Pages 1 - 8

https://doi.org/10.1145/2966986.2980087

Published: 07 November 2016 Publication History

Abstract

Formal techniques seem to be a way to cope with the exploding complexity of functional safety analysis. Here, the overall fault propagation probability to a certain safety-point in the design must be analyzed. As a consequence, the careful verification of the design is no longer sufficient. In addition, the propagation of all possible faults potentially showing up at all of the design's internal nodes must be validated. But this is not only a complexity challenge. Safety standards have a probabilistic view on functional safety analysis results and aspects such as different fault and pattern probability must be considered and related to requirements such as confidence level and maximum FIT rate. Following an overview on verification challenges around functional safety analysis, we introduce our innovative concept on how formal formal techniques can substantially simplify industrial functional safety analysis ows.

References

[1]

Christel Baier, Joost-Pieter Katoen, and Kim Guldstrand Larsen. Principles of model checking. MIT press, 2008.

Digital Library

[2]

Robert C Baumann. Radiation-induced soft errors in advanced semiconductor technologies. IEEE Transactions on Device and materials reliability, 5 (3): 305–316, 2005.

[3]

Alessandro Bernardini and Ulf Schlichtmann. Symbolic fault modeling and model counting for the identification of critical gates in digital circuits. In ZuE 2015; 8. GMM/ITG/GI-Symposium Reliability by Design; Proceedings of, pages 1–8. VDE, 2015.

[4]

A. Biere. Aiger format. http://fmv.jku.at/aiger/FORMAT, 2007.

[5]

A. Biere and K.L. Claessen. Hardware model checking competition (hwmcc) benchmarks. http://fmv.jku.at/hwmcc15/.

[6]

Aaron R Bradley. Understanding ic3. In International Conference on Theory and Applications of Satisfiability Testing, pages 1–14. Springer, 2012.

[7]

Robert Brayton and Alan Mishchenko. Abc: An academic industrial-strength verification tool. In International Conference on Computer Aided Verification, pages 24–40. Springer, 2010.

[8]

Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Ic3 modulo theories via implicit predicate abstraction. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 46–61. Springer, 2014.

[9]

Edmund M Clarke, Orna Grumberg, and Doron Peled. Model checking. MIT press, 1999.

Digital Library

[10]

William L Dunn and J. Kenneth Shultis. Exploring Monte Carlo Methods. Elsevier 2011.

[11]

Mojtaba Ebrahimi, Nour Sayed, Maryam Rashvand, and Mehdi B Tahoori. Fault injection acceleration by architectural importance sampling. In Proceedings of the 10th International Conference on Hardware/Software Codesign and System Synthesis, pages 212–219. IEEE Press, 2015.

[12]

Niklas Een, Alan Mishchenko, and Robert Brayton. Efficient implementation of property directed reachability. In Formal Methods in Computer-Aided Design (FMCAD), 2011, pages 125–134. IEEE, 2011.

[13]

Richard L Graham, Timothy S Woodall, and Jeffrey M Squyres. Open mpi: A flexible high performance mpi. In International Conference on Parallel Processing and Applied Mathematics, pages 228–239. Springer, 2005.

[14]

Alberto Griggio and Marco Roveri. Comparing different variants of the ic3 algorithm for hardware model checking. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 35 (6): 1026–1039, 2016.

Digital Library

[15]

Mei-Chen Hsueh, Timothy K Tsai, and Ravishankar K Iyer. Fault injection techniques and tools. Computer, 30 (4): 75–82, 1997.

Digital Library

[16]

Orna Kupferman and Moshe Y Vardi. Model checking of safety properties. Formal Methods in System Design, 19 (3): 291–314, 2001.

Digital Library

[17]

Natasa Miskov-Zivanov and Diana Marculescu. Circuit reliability analysis using symbolic techniques. Computer-Aided Design of Integrated Circuits and Systems, IEEE Transactions on, 25 (12): 2638–2649, 2006.

Digital Library

[18]

Shubhendu S Mukherjee, Christopher Weaver, Joel Emer, Steven K Reinhardt, and Todd Austin. A systematic methodology to compute the architectural vulnerability factors for a high-performance microprocessor. In Proceedings of the 36th annual IEEE/ACM International Symposium on Microarchitecture, page 29. IEEE Computer Society, 2003.

Digital Library

[19]

Art B. Owen. Monte carlo theory, methods and examples. http://statweb.stanford.edu/-owen/mc/, 2013.

[20]

Sanjit A Seshia, Wenchao Li, and Subhasish Mitra. Verification-guided soft error resilience. In Proceedings of the conference on Design, automation and test in Europe, pages 1442–1447. EDA Consortium, 2007.

[21]

S.Z. Shazli and M.B. Tahoori. Using boolean satisfiability for computing soft error rates in early design stages. Microelectronics Reliability, 50 (1): 149–159, 2010.

[22]

B-A. Tabacaru, M. Chaari, W. Ecker, T. Kruse, and C. Novello. Safety analysis on multiple abstraction levels. Invited Presentation at Design Automation and Test in Europe, DATE16, March 16. 2016.

Cited By

Zhang XXiao SXia YLi JChen MPu G(2023)Accelerate Safety Model Checking Based on Complementary Approximate ReachabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.323627242:9(3105-3117)Online publication date: Sep-2023
https://doi.org/10.1109/TCAD.2023.3236272
Sarkar AChakrabarty JAlthaf M(2023)Design of a Rugged Radiating Panel Assembly with High Reliability2023 IEEE Microwaves, Antennas, and Propagation Conference (MAPCON)10.1109/MAPCON58678.2023.10463946(1-6)Online publication date: 11-Dec-2023
https://doi.org/10.1109/MAPCON58678.2023.10463946
Xiao SZhang CLi JPu G(2023)FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 FormatTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_5(36-43)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_5
Show More Cited By

Index Terms

Where formal verification can help in functional safety analysis

Index terms have been assigned to the content through auto-classification.

Recommendations

Formal verification of ASMs using MDGs

We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Integrated formal verification of safety-critical software

This work presents a formal verification process based on the Systerel Smart Solver (S3) toolset for the development of safety-critical embedded software. In order to guarantee the correctness of the implementation of a set of textual requirements, the ...
Coverage metrics for formal verification

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

2016 IEEE/ACM International Conference on Computer-Aided Design (ICCAD)

Nov 2016

946 pages

Copyright © 2016.

Publisher

IEEE Press

Publication History

Published: 07 November 2016

Permissions

Request permissions for this article.

Request Permissions

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

13
Total Citations
View Citations
121
Total Downloads

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

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Zhang XXiao SXia YLi JChen MPu G(2023)Accelerate Safety Model Checking Based on Complementary Approximate ReachabilityIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2023.323627242:9(3105-3117)Online publication date: Sep-2023
https://doi.org/10.1109/TCAD.2023.3236272
Sarkar AChakrabarty JAlthaf M(2023)Design of a Rugged Radiating Panel Assembly with High Reliability2023 IEEE Microwaves, Antennas, and Propagation Conference (MAPCON)10.1109/MAPCON58678.2023.10463946(1-6)Online publication date: 11-Dec-2023
https://doi.org/10.1109/MAPCON58678.2023.10463946
Xiao SZhang CLi JPu G(2023)FuzzBtor2: A Random Generator of Word-Level Model Checking Problems in Btor2 FormatTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-031-30820-8_5(36-43)Online publication date: 22-Apr-2023
https://dl.acm.org/doi/10.1007/978-3-031-30820-8_5
Bagbaba AAugusto da Silva FSonza Reorda MHamdioui SJenihhin MSauer C(2022)Automated Identification of Application-Dependent Safe Faults in Automotive Systems-on-a-ChipsElectronics10.3390/electronics1103031911:3(319)Online publication date: 20-Jan-2022
https://doi.org/10.3390/electronics11030319
Bartsch CWilhelm SKastner DStoffel DKunz W(2021)Compositional Fault Propagation Analysis in Embedded Systems using Abstract Interpretation2021 IEEE International Test Conference (ITC)10.1109/ITC50571.2021.00057(409-418)Online publication date: Oct-2021
https://doi.org/10.1109/ITC50571.2021.00057
da Silva FBagbaba AHamdioui SSauer C(2021)Flip Flop Weighting: A technique for estimation of safety metrics in Automotive Designs2021 IEEE 27th International Symposium on On-Line Testing and Robust System Design (IOLTS)10.1109/IOLTS52814.2021.9486697(1-7)Online publication date: 28-Jun-2021
https://doi.org/10.1109/IOLTS52814.2021.9486697
da Silva FBagbaba ASartoni SCantoro RReorda MHamdioui SSauer C(2020)Determined-Safe Faults Identification: A step towards ISO26262 hardware compliant designs2020 IEEE European Test Symposium (ETS)10.1109/ETS48528.2020.9131568(1-6)Online publication date: May-2020
https://doi.org/10.1109/ETS48528.2020.9131568
Dureja RLi JPu GVardi MRozier K(2020)Intersection and Rotation of Assumption Literals Boosts Bug-FindingVerified Software. Theories, Tools, and Experiments10.1007/978-3-030-41600-3_12(180-192)Online publication date: 14-Mar-2020
https://doi.org/10.1007/978-3-030-41600-3_12
Xu ZAbraham J(2019)Resilient Reorder Buffer Design for Network-on-Chip20th International Symposium on Quality Electronic Design (ISQED)10.1109/ISQED.2019.8697766(92-97)Online publication date: Mar-2019
https://doi.org/10.1109/ISQED.2019.8697766
Li JDureja RPu GRozier KVardi M(2018)SimpleCAR: An Efficient Bug-Finding Tool Based on Approximate ReachabilityComputer Aided Verification10.1007/978-3-319-96142-2_5(37-44)Online publication date: 18-Jul-2018
https://doi.org/10.1007/978-3-319-96142-2_5
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents