Advertisement

Robust Digital Computation in the Physical World

  • Jackson R. Mayo
  • Robert C. Armstrong
  • Geoffrey C. Hulette
  • Maher Salloum
  • Andrew M. Smith
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.

Notes

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.

References

  1. 1.
    J.R. Abrial, Modeling in Event-B: System and Software Engineering, 1st edn. (Cambridge University Press, Cambridge, 2010)CrossRefGoogle Scholar
  2. 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–229CrossRefGoogle Scholar
  3. 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)CrossRefGoogle Scholar
  4. 4.
    Y. Bertot, P. Castéran, Interactive Theorem Proving and Program Development (Springer, Heidelberg, 2004)CrossRefGoogle Scholar
  5. 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–304Google Scholar
  6. 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)CrossRefGoogle Scholar
  7. 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. 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–364Google Scholar
  9. 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)MathSciNetCrossRefGoogle Scholar
  10. 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–158Google Scholar
  11. 11.
    P. Derler, E.A. Lee, A. Sangiovanni-Vincentelli, Modeling cyber-physical systems. Proc. IEEE (special issue on CPS) 100(1), 13–28 (2012)CrossRefGoogle Scholar
  12. 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–56Google Scholar
  13. 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–292Google Scholar
  14. 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. 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)MathSciNetCrossRefGoogle Scholar
  16. 16.
    M. Jackson, P. Zave, Deriving specifications from requirements: an example, in Proceedings of the 17th International Conference on Software Engineering (1995), pp. 15–24Google Scholar
  17. 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. 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. 19.
    S.A. Kauffman, The Origins of Order: Self-organization and Selection in Evolution (Oxford University Press, Oxford, 1993)Google Scholar
  20. 20.
    L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers (Addison-Wesley, Boston, 2002)Google Scholar
  21. 21.
    L. Lamport, Buridan’s principle. Found. Phys. 42(8), 1056–1066 (2012)CrossRefGoogle Scholar
  22. 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–114Google Scholar
  23. 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–186Google Scholar
  24. 24.
    T. Mytkowicz, A. Diwan, E. Bradley, Computer systems are dynamical systems. Chaos 19, 033124 (2009)CrossRefGoogle Scholar
  25. 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–178Google Scholar
  26. 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. 27.
    H.G. Rice, Classes of recursively enumerable sets and their decision problems. Trans. Am. Math. Soc. 74(2), 358–366 (1953)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Y. Saad, Iterative Methods for Sparse Linear Systems, 2nd edn. (SIAM, Philadelphia, 2003)CrossRefGoogle Scholar
  29. 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. 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–371Google Scholar
  31. 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–1447Google Scholar
  32. 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. 33.
    The Coq development team, The Coq proof assistant reference manual (2004). http://coq. inria.fr
  34. 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–892Google Scholar
  35. 35.
    J. Woodcock, P.G. Larsen, J. Bicarregui, J. Fitzgerald, Formal methods: practice and experience. ACM Comput. Surv. 41, 19 (2009)CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Jackson R. Mayo
    • 1
  • Robert C. Armstrong
    • 1
  • Geoffrey C. Hulette
    • 1
  • Maher Salloum
    • 1
  • Andrew M. Smith
    • 1
  1. 1.Sandia National LaboratoriesLivermoreUSA

Personalised recommendations