Skip to main content
SpringerLink
Log in
Book cover

Cyber-Physical Systems Security pp 1–21Cite as

Robust Digital Computation in the Physical World

  • Chapter

Abstract

Modern digital hardware and software designs are increasingly complex but are themselves only idealizations of a real system that is instantiated in, and interacts with, an analog physical environment. Insights from physics, formal methods, and complex systems theory can aid in extending reliability and security measures from pure digital computation (itself a challenging problem) to the broader cyber-physical and out-of-nominal arena. Example applications to design and analysis of high-consequence controllers and extreme-scale scientific computing illustrate the interplay of physics and computation. In particular, we discuss the limitations of digital models in an analog world, the modeling and verification of out-of-nominal logic, and the resilience of computational physics simulation. A common theme is that robustness to failures and attacks is fostered by cyber-physical system designs that are constrained to possess inherent stability or smoothness. This chapter contains excerpts from previous publications by the authors.

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   129.00
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD   169.99
Price excludes VAT (USA)
  • Durable hardcover 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. J.R. Abrial, Modeling in Event-B: System and Software Engineering, 1st edn. (Cambridge University Press, Cambridge, 2010)

    Book  Google Scholar 

  2. R. Alur, C. Courcoubetis, T.A. Henzinger, P.H. Ho, Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems, in Hybrid Systems, ed. by R.L. Grossman, A. Nerode, A.P. Ravn, H. Rischel. Lecture Notes in Computer Science, vol. 736 (Springer, Heidelberg, 1993), pp. 209–229

    Chapter  Google Scholar 

  3. J.C. Barros, B.W. Johnson, Equivalence of the arbiter, the synchronizer, the latch, and the inertial delay. IEEE Trans. Comput. 32(7), 603–614 (1983)

    Article  Google Scholar 

  4. Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development (Springer, Heidelberg, 2004)

    Book  Google Scholar 

  5. S. Boldo, C. Lelay, G. Melquiond, Improving real analysis in Coq: a user-friendly approach to integrals and derivatives, in CPP’12, ed. by C. Hawblitzel, D. Miller. Lecture Notes in Computer Science, vol. 7679 (Springer, Heidelberg, 2012), pp. 289–304

    Google Scholar 

  6. G. Bosilca, R. Delmas, J. Dongarra, J. Langou, Algorithm-based fault tolerance applied to high performance computing. J. Parallel Distrib. Comput. 69, 410–416 (2009)

    Article  Google Scholar 

  7. F. Cappello, A. Geist, W. Gropp, S. Kale, B. Kramer, M. Snir, Toward exascale resilience: 2014 update. Supercomput. Front. Innov. 1(1), 5–28 (2014)

    Google Scholar 

  8. A. Cimatti, E.M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, A. Tacchella, NuSMV 2: an opensource tool for symbolic model checking, in Proceedings of the 14th International Conference on Computer Aided Verification (2002), pp. 359–364

    Google Scholar 

  9. E. Clarke, O. Grumberg, S. Jha, Y. Lu, H. Veith, Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 752–794 (2003)

    Article  MathSciNet  Google Scholar 

  10. S.A. Cook, The complexity of theorem-proving procedures, in Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (1971), pp. 151–158

    Google Scholar 

  11. P. Derler, E.A. Lee, A. Sangiovanni-Vincentelli, Modeling cyber-physical systems. Proc. IEEE (special issue on CPS) 100(1), 13–28 (2012)

    Article  Google Scholar 

  12. G. Fey, Assessing system vulnerability using formal verification techniques, in Mathematical and Engineering Methods in Computer Science, ed. by Z. Kotásek, J. Bouda, I. Černá, L. Sekanina, T. Vojnar, D. Antoš. Lecture Notes in Computer Science, vol. 7119 (Springer, Heidelberg, 2012), pp. 47–56

    Google Scholar 

  13. T.A. Henzinger, The theory of hybrid automata, in Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (1996), pp. 278–292

    Google Scholar 

  14. M.A. Heroux, D.W. Doerfler, P.S. Crozier, J.M. Willenbring, C. Edwards, A. Williams, M. Rajan, E.R. Keiter, H.K. Thornquist, R.W. Numrich, Improving performance via mini-applications. Report SAND2009-5574, Sandia National Laboratories (2009)

    Google Scholar 

  15. G.C. Hulette, R.C. Armstrong, J.R. Mayo, J.R. Ruthruff, Theorem-proving analysis of digital control logic interacting with continuous dynamics. Electron. Notes Theor. Comput. Sci. 317, 71–83 (2015)

    Article  MathSciNet  Google Scholar 

  16. M. Jackson, P. Zave, Deriving specifications from requirements: an example, in Proceedings of the 17th International Conference on Software Engineering (1995), pp. 15–24

    Google Scholar 

  17. A. Joshi, S.P. Miller, M. Whalen, M.P. Heimdahl, A proposal for model-based safety analysis, in Proceedings of the 24th Digital Avionics Systems Conference (2005)

    Google Scholar 

  18. A. Joshi, M.P.E. Heimdahl, S.P. Miller, M.W. Whalen, Model-based safety analysis. NASA Contractor Report CR-2006-213953 (2006)

    Google Scholar 

  19. S.A. Kauffman, The Origins of Order: Self-organization and Selection in Evolution (Oxford University Press, Oxford, 1993)

    Google Scholar 

  20. L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley, Boston, 2002)

    Google Scholar 

  21. L. Lamport, Buridan’s principle. Found. Phys. 42(8), 1056–1066 (2012)

    Article  Google Scholar 

  22. J.R. Mayo, R.C. Armstrong, G.C. Hulette, Digital system robustness via design constraints: the lesson of formal methods, in Proceedings of the 9th Annual IEEE International Systems Conference (2015), pp. 109–114

    Google Scholar 

  23. J.R. Mayo, R.C. Armstrong, G.C. Hulette, Leveraging abstraction to establish out-of-nominal safety properties, in Proceedings of the 4th International Workshop on Formal Techniques for Safety-Critical Systems, ed. by C. Artho, P.C. Ölveczky. Communications in Computer and Information Science, vol. 596 (Springer, Heidelberg, 2016), pp. 172–186

    Google Scholar 

  24. T. Mytkowicz, A. Diwan, E. Bradley, Computer systems are dynamical systems. Chaos 19, 033124 (2009)

    Article  Google Scholar 

  25. A. Platzer, J.D. Quesel, KeYmaera: a hybrid theorem prover for hybrid systems, in Automated Reasoning, ed. by A. Armando, P. Baumgartner, G. Dowek. Lecture Notes in Computer Science, vol. 5195 (Springer, Heidelberg, 2008), pp. 171–178

    Google Scholar 

  26. J. Ray, J.R. Mayo, R.C. Armstrong, Finite difference stencils robust to silent data corruption, in SIAM Conference on Parallel Processing for Scientific Computing (2014). https://www.pathlms.com/siam/courses/477/sections/716

  27. H.G. Rice, Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74(2), 358–366 (1953)

    Article  MathSciNet  Google Scholar 

  28. Y. Saad, Iterative Methods for Sparse Linear Systems, 2nd edn. (SIAM, Philadelphia, 2003)

    Book  Google Scholar 

  29. M. Salloum, J.R. Mayo, R.C. Armstrong, In-situ mitigation of silent data corruption in PDE solvers, in Proceedings of the 6th Workshop on Fault Tolerance for HPC at Extreme Scale (2016)

    Google Scholar 

  30. M.U. Sanwal, O. Hasan, Formal verification of cyber-physical systems: coping with continuous elements, in ICCSA’13, ed. by B. Murgante, S. Misra, M. Carlini, C.M. Torre, H.Q. Nguyen, D. Taniar, B.O. Apduhan, O. Gervasi. Lecture Notes in Computer Science, vol. 7971 (Springer, Heidelberg, 2013), pp. 358–371

    Google Scholar 

  31. S.A. Seshia, W. Li, S. Mitra, Verification-guided soft error resilience, in Proceedings of the Conference on Design, Automation and Test in Europe (2007), pp. 1442–1447

    Google Scholar 

  32. P. Strazdins, B. Harding, C. Lee, J.R. Mayo, J. Ray, R.C. Armstrong, A robust technique to make a 2D advection solver tolerant to soft faults, in Proceedings of the International Conference on Computational Science (2016)

    Google Scholar 

  33. The Coq development team, The Coq proof assistant reference manual (2004). http://coq. inria.fr

  34. O. Tveretina, Towards the safety verification of real-time systems with the Coq proof assistant, in Proceedings of the International Multiconference on Computer Science and Information Technology, vol. 2 (2007), pp. 883–892

    Google Scholar 

  35. J. Woodcock, P.G. Larsen, J. Bicarregui, J. Fitzgerald, Formal methods: practice and experience. ACM Comput. Surv. 41, 19 (2009)

    Article  Google Scholar 

Download references

Acknowledgements

Sandia National Laboratories is a multimission laboratory managed and operated by National Technology and Engineering Solutions of Sandia LLC, a wholly owned subsidiary of Honeywell International Inc., for the US Department of Energy’s National Nuclear Security Administration (NNSA) under contract DE-NA0003525. This work was funded by NNSA’s Advanced Simulation and Computing (ASC) Program.

Author information

Authors and Affiliations

  1. Sandia National Laboratories, Livermore, CA, USA

    Jackson R. Mayo, Robert C. Armstrong, Geoffrey C. Hulette, Maher Salloum & Andrew M. Smith

Authors
  1. Jackson R. Mayo
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Robert C. Armstrong
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Geoffrey C. Hulette
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Maher Salloum
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Andrew M. Smith
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jackson R. Mayo .

Editor information

Editors and Affiliations

  1. İstinye University, İstanbul, Turkey

    Çetin Kaya Koç

  2. Nanjing University of Aeronautics and Astronautics, Nanjing, China

    Çetin Kaya Koç

  3. University of California Santa Barbara, Santa Barbara, CA, USA

    Çetin Kaya Koç

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Cite this chapter

Mayo, J.R., Armstrong, R.C., Hulette, G.C., Salloum, M., Smith, A.M. (2018). Robust Digital Computation in the Physical World. In: Koç, Ç.K. (eds) Cyber-Physical Systems Security. Springer, Cham. https://doi.org/10.1007/978-3-319-98935-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-98935-8_1

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-98934-1

  • Online ISBN: 978-3-319-98935-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation