×

Feasibility analysis for robustness quantification by symbolic model checking. (English) Zbl 1247.68156

Summary: We propose and investigate a robustness evaluation procedure for sequential circuits subject to particle strikes inducing bit-flips in memory elements. We define a general fault model, a parametric reparation model and quantitative measures reflecting the robustness capability of the circuit with respect to these fault and reparation models. We provide algorithms to compute these metrics and show how they can be interpreted in order to better understand the robustness capability of several circuits (a simple circuit coming from the VIS distribution, circuits from the itc-99 benchmarks and a CAN-Bus interface).

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
94C12 Fault detection; testing in circuits and networks

Software:

sharpSAT
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abke J, Bohl E, Henno C (1998) Emulation based real time testing of automotive applications. In: Proc of 4th IEEE international on-line testing workshop, pp 28–31
[2] Baarir S, Braunstein C, Clavel R, Encrenaz E, Ilié J-M, Leveugle R, Mounier I, Pierre L, Poitrenaud D (2009) Complementary formal approaches for dependability analysis. In: Proc international symposium on defect and fault tolerance in VLSI systems. IEEE Comput Soc, Los Alamitos, pp 331–339
[3] Bidgoli H (2006) Handbook of information security, vol 3. Wiley, New York
[4] Biere A, Cimatti A, Clarke EM, Zhu Y (1999) Symbolic model checking without BDDs. In: Proc international conference on tools and algorithms for construction and analysis of systems. Lecture notes in computer science, vol 1579. Springer, Berlin, pp 193–207
[5] Birnbaum E, Lozinskii EL (1999) The good old Davis-Putnam procedure helps counting models. J Artif Intell Res 10:457–477 · Zbl 0918.68098
[6] Church A (1957) Application of recursive arithmetic to the problem of circuit synthesis. In: Summaries of talks presented at the summer institute for symbolic logic. Princeton. Communications Research Division, Institute for Defense Analyses, Princeton, pp 3–50
[7] Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244–263 · Zbl 0591.68027 · doi:10.1145/5397.5399
[8] Corno F, Sonza Reorda M, Squillero G (2000) RT-level ITC 99 benchmarks and first ATPG results. IEEE Des Test Comput 17(3):44–53 · Zbl 05093410 · doi:10.1109/54.867894
[9] Daveau J-M, Blampey A, Gasiot G, Bulone J, Roche P (2009) An industrial fault injection platform for soft-error dependability analysis and hardening of complex system-on-a-chip. In: IEEE RPS-CDR 47th annu int reliability physics symp, Montreal, Canada. IEEE Press, New York
[10] Davis RI, Burns A, Bril R, Lukkien J (2007) Controller area network (can) schedulability analysis: Refuted, revisited and revised. Real-Time Syst 35(3):239–272 · Zbl 05131256 · doi:10.1007/s11241-007-9012-7
[11] Dijkstra EW (1974) Self-stabilization systems in spite of distributed control. Commun ACM 17:643–644 · Zbl 0305.68048 · doi:10.1145/361179.361202
[12] Dolev S (2000) Self-stabilization. MIT Press, Cambridge · Zbl 1026.93001
[13] Fey G, Drechsler R (2008) A basis for formal robustness checking. In: Proc IEEE international symposium on quality electronic design. IEEE Comput Soc, Los Alamitos, pp 784–789
[14] Fey G, Sülflow A, Drechsler R (2009) Computing bounds for fault tolerance using formal techniques. In: Proc design automation conference. ACM, New York, pp 190–195
[15] Garcia-Valderas M, Portela-Garcia M, Lopez-Ongil C, Entrena L (2010) Extensive SEU impact analysis of a pic microprocessor for selective hardening. IEEE Trans Nucl Sci 57(4)
[16] Hopcroft JE, Motwani R, Ullman JD (2006) Introduction to automata theory, languages, and computation (3rd edn.). Addison-Wesley/Longman, Boston
[17] ISO technical committees TC22/SC3 (2003) Road vehicles–controller area networks–parts 1 to 5. International Organization for Standardization, Geneva
[18] Jenn E, Arlat J, Rimen R, Ohlsson J, Karlsson J (1994) Fault injection into VHDL models: the MEPHISTO tool. In: Proc of 24th symposium on fault-tolerant computing (FTCS), pp 66–75
[19] Krautz U, Pflanz M, Jacobi C, Tast H, Weber K, Vierhaus H (2006) Evaluating coverage of error detection logic for soft errors using formal methods. In: Proc conference on design, automation and test in Europe. European Design and Automation Association, pp 176–181
[20] Krishnaswamy S, Viamontes GF, Markov IL, Hayes J (2008) Probabilistic transfert matrices in symbolic reliability analysis of logic circuits for reliability evaluation of logic circuits. Trans Des Autom Electron Syst 13(1)
[21] Leveugle R (2005) A new approach for early dependability evaluation based on formal property checking and controlled mutation. In: Proc IEEE international on-line testing symposium. IEEE Comput Soc, Los Alamitos, pp 260–265
[22] Leveugle R, Hadjiat K (2003) Multi-level fault injections in VHDL descriptions: alternative approaches and experiments. J Electron Test Theory Appl. 19(5):559–575 · doi:10.1023/A:1025178014797
[23] Leveugle R, Calvez A, Maistri P, Vanhauwaert P (2009) Statistical fault injection: quantified error and confidence. In: Proc of design, automation and test in Europe conference (DATE), pp 502–506
[24] Lopez-Ongil C, Garcia-Valderas M, Portela-Garcia M, Entrena L (2007) Autonomous fast emulation: a new FPGA-based acceleration system for hardness evaluation. IEEE Trans Nucl Sci 54(1)
[25] Naviner L, Naviner JF, Franco D, Vasconcelos M (2008) Signal probability for reliability evaluation of logic circuits. Microelectron Reliab J 48
[26] Naviner L, Naviner JF, Goncalves dos Santos G Jr, Crespo Marques E (2010) Using error tolerance of target application for efficient reliability improvement of digital circuits. Microelectron Reliab J 50(9–11)
[27] Polian I, Hayes JP, Sudhakar MR, Becker B (2010) Modeling and mitigating transient errors in logic circuits. IEEE Trans Dependable and Secure Comput 99(PrePrints)
[28] Seshia S, Li W, Mitra S (2007) Verification-guided soft error resilience. In: Proc conference on design, automation and test in Europe. EDA Consortium, San Jose, pp 1442–1447
[29] Shtrichman O (2000) Tuning SAT checkers for bounded model checking. In: Proc international conference on computer aided verification. Lecture notes in computer science, vol 1855. Springer, Berlin, pp 480–494 · Zbl 0974.68565
[30] The VIS group (1996) VIS: a system for verification and synthesis. In: Proc international conference on computer aided verification. Lecture notes in computer science, vol 1102. Springer, Berlin, pp 428–432
[31] Thurley M (2006) sharpSAT–counting models with advanced component caching and implicit BCP. In: Theory and applications of satisfiability testing (SAT’06). Lecture notes in computer science, vol 4121. Seattle, WA, USA, August 2006. Springer, Berlin, pp 424–429
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.