Skip to main content
SpringerLink
Log in
Book cover

From Software Engineering to Formal Methods and Tools, and Back pp 531–547Cite as

Application of Model Checking to Fault Tolerance Analysis

  • Chapter
  • First Online:

  • 1176 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11865))

Abstract

A basic concept in modeling fault tolerant systems is that anticipated faults, being obviously outside of our control, may or may not occur. A fault tolerant system design can be proved to correctly behave under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault-free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behavior can be applied to verify the correctness of the design. Another activity that must be considered in fault tolerance is the issue of fault detection, since the existence of undetectable faults makes the system more vulnerable. The usage of model checking and temporal logic gives opportunities to better analyze the system behavior in presence of faults and to identify undetectable faults.

Work partially supported by the Italian Ministry of Education and Research (MIUR) in the framework of the CrossLab project (Departments of Excellence).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Battezzati, N., Sterpone, L., Violante, M.: Reconfigurable Field Programmable Gate Arrays for Mission-Critical Application. Springer, New York (2011). https://doi.org/10.1007/978-1-4419-7595-9

    Book  Google Scholar 

  2. Baumann, R.C.: Radiation-induced soft errors in advanced semiconductor technologies. IEEE Trans. Device Mater. Reliab. 5(3), 305–316 (2005). https://doi.org/10.1109/TDMR.2005.853449

    Article  Google Scholar 

  3. Bernardeschi, C., Cassano, L., Cimino, M.G., Domenici, A.: GABES: a genetic algorithm based environment for SEU testing in SRAM-FPGAs. J. Syst. Architect. 59(10, Part D), 1383–1254 (2013). https://doi.org/10.1016/j.sysarc.2013.10.006, http://www.sciencedirect.com/science/article/pii/S1383762113001975

  4. Bernardeschi, C., Cassano, L., Domenici, A.: SEU-X: a SEU un-excitability prover for SRAM-FPGAs. In: 18th IEEE International On-Line Testing Symposium, IOLTS 2012, pp. 25–30 (2012)

    Google Scholar 

  5. Bernardeschi, C., Cassano, L., Domenici, A., Sterpone, L.: Unexcitability analysis of SEus affecting the routing structure of SRAM-based FPGAs. In: Great Lakes Symposium on VLSI 2013 (part of ECRC), GLSVLSI 2013, Paris, 2–4 May 2013, pp. 7–12 (2013)

    Google Scholar 

  6. Bernardeschi, C., Cassano, L., Domenici, A., Sterpone, L.: UA\({}^{\text{2 }}\)TPG: an untestability analyzer and test pattern generator for SEUs in the configuration memory of SRAM-based FPGAs. Integration 55, 85–97 (2016). https://doi.org/10.1016/j.vlsi.2016.03.004

    Google Scholar 

  7. Bernardeschi, C., Fantechi, A., Gnesi, S.: Formal validation of the GUARDS inter-consistency mechanism. In: Felici, M., Kanoun, K. (eds.) SAFECOMP 1999. LNCS, vol. 1698, pp. 420–430. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48249-0_36

    Chapter  Google Scholar 

  8. Bernardeschi, C., Fantechi, A., Gnesi, S.: Formal validation of fault-tolerance mechanisms inside GUARDS. Reliab. Eng. Syst. Saf. 71(3), 261–270 (2001). https://doi.org/10.1016/S0951-8320(00)00078-8

    Article  Google Scholar 

  9. Bernardeschi, C., Fantechi, A., Simoncini, L.: Formally verifying fault tolerant system designs. Comput. J. 43(3), 191–205 (2000). https://doi.org/10.1093/comjnl/43.3.191

    Article  MATH  Google Scholar 

  10. Bouali, A., Gnesi, S., Larosa, S.: The integration project for the JACK environment. Technical report CS-R9443, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands (1994)

    Google Scholar 

  11. Boudol, G.: Notes on algebraic calculi of processes. In: Apt, K. (ed.) Logics and Models of Concurrent Systems. NATO ASI Series (Series F: Computer and Systems Sciences), vol. 13, pp. 261–303. Springer, Heidelberg (1985). https://doi.org/10.1007/978-3-642-82453-1_9

    Chapter  Google Scholar 

  12. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. 8(2), 244–263 (1986). https://doi.org/10.1145/5397.5399

    Article  MATH  Google Scholar 

  13. De Nicola, R., Fantechi, A., Gnesi, S., Ristori, G.: An action based framework for verifying logical and behavioural properties of concurrent systems. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 37–47. Springer, Heidelberg (1992). https://doi.org/10.1007/3-540-55179-4_5

    Chapter  Google Scholar 

  14. Dutertre, B., Sorea, M.: Modeling and verification of a fault-tolerant real-time startup protocol using calendar automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp. 199–214. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30206-3_15

    Chapter  MATH  Google Scholar 

  15. Francalanza, A., Hennessy, M.: A theory of system behaviour in the presence of node and link failures. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 368–382. Springer, Heidelberg (2005). https://doi.org/10.1007/11539452_29

    Chapter  MATH  Google Scholar 

  16. Gnesi, S., Lenzini, G., Martinelli, F.: Logical specification and analysis of fault tolerant systems through partial model checking. Electron. Notes Theor. Comput. Sci. 118, 57–70 (2005). https://doi.org/10.1016/j.entcs.2004.09.032

    Article  MATH  Google Scholar 

  17. Graham, P., Caffrey, M., Zimmerman, J., Sundararajan, P., Johnson, E.: Consequences and categories of SRAM FPGA configuration SEUs. In: In Proceedings of the International Conference on Military and Aerospace Programmable Logic Devices (MAPLD 2003 (2003)

    Google Scholar 

  18. Hennessy, M., Riely, J.: Resource access control in systems of mobile agents. Inf. Comput. 173(1), 82–120 (2002). https://doi.org/10.1006/inco.2001.3089

    Article  MathSciNet  MATH  Google Scholar 

  19. Holzmann, G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997). https://doi.org/10.1109/32.588521

    Article  Google Scholar 

  20. Janowski, T.: On bisimulation, fault-monotonicity and provable fault-tolerance. In: Johnson, M. (ed.) AMAST 1997. LNCS, vol. 1349, pp. 292–306. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0000478

    Chapter  Google Scholar 

  21. John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Towards modeling and model checking fault-tolerant distributed algorithms. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 209–226. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39176-7_14

    Chapter  Google Scholar 

  22. Jones, B.F., Pike, L.: Modular model-checking of a byzantine fault-tolerant protocol. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 163–177. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_12

    Chapter  Google Scholar 

  23. Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems - Specification. Springer, Heidelberg (1992). https://doi.org/10.1007/978-1-4612-0931-7

    Book  MATH  Google Scholar 

  24. Milner, R.: Communication and Concurrency. Prentice-Hall Inc, Upper Saddle River (1989)

    MATH  Google Scholar 

  25. de Moura, L., et al.: SAL 2. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 496–500. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27813-9_45

    Chapter  Google Scholar 

  26. Powell, D., et al.: GUARDS: a generic upgradable architecture for real-time dependable systems. IEEE Trans. Parallel Distrib. Syst. 10(6), 580–599 (1999). https://doi.org/10.1109/71.774908

    Article  Google Scholar 

  27. Rodriguez-Andina, J., Moure, M., Valdes, M.: Features, design tools, and application domains of FPGAs. IEEE Trans. Industr. Electron. 54(4), 1810–1823 (2007). https://doi.org/10.1109/TIE.2007.898279

    Article  Google Scholar 

  28. Sterpone, L., et al.: Experimental validation of a tool for predicting the effects of soft errors in SRAM-based FPGAs. IEEE Trans. Nucl. Sci. 54(6), 2576–2583 (2007). https://doi.org/10.1109/TNS.2007.910122

    Article  Google Scholar 

Download references

Acknowledgments

Working with Stefania has been both a challenge and a pleasure. Her rigorous approach, knowledge, experience and insight, together with her collaborative attitude and general friendliness have been a source of inspiration and motivation not only behind the work done together, but also in other research fields.

Author information

Authors and Affiliations

  1. Department of Information Engineering, University of Pisa, Pisa, Italy

    Cinzia Bernardeschi & Andrea Domenici

Authors
  1. Cinzia Bernardeschi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andrea Domenici
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Cinzia Bernardeschi .

Editor information

Editors and Affiliations

  1. Consiglio Nazionale delle Ricerche, Pisa, Italy

    Maurice H. ter Beek

  2. Università degli Studi di Firenze, Florence, Italy

    Alessandro Fantechi

  3. Università di Pisa, Pisa, Italy

    Laura Semini

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Bernardeschi, C., Domenici, A. (2019). Application of Model Checking to Fault Tolerance Analysis. In: ter Beek, M., Fantechi, A., Semini, L. (eds) From Software Engineering to Formal Methods and Tools, and Back. Lecture Notes in Computer Science(), vol 11865. Springer, Cham. https://doi.org/10.1007/978-3-030-30985-5_31

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-30985-5_31

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-30984-8

  • Online ISBN: 978-3-030-30985-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation