Advertisement

Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System

  • Philip Johnson-FreydEmail author
  • Geoffrey C. Hulette
  • Zena M. Ariola
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9933)

Abstract

Sandia engineers use the Temporal Logic of Actions (TLA) early in the design process for digital systems where safety considerations are critical. TLA allows us to easily build models of interactive systems and prove (in the mathematical sense) that those models can never violate safety requirements, all in a single formal language. TLA models can also be refined, that is, extended by adding details in a carefully prescribed way, such that the additional details do not break the original model. Our experience suggests that engineers using refinement can build, maintain, and prove safety for designs that are significantly more complex than they otherwise could. We illustrate the way in which we have used TLA, including refinement, with a case study drawn from a real safety-critical system. This case exposes a need for refinement by composition, which is not currently provided by TLA. We have extended TLA to support this kind of refinement by building a specialized version of it in the Coq theorem prover. Taking advantage of Coq’s features, our version of TLA exhibits other benefits over stock TLA: we can prove certain difficult kinds of safety properties using mathematical induction, and we can certify the correctness of our proofs.

Keywords

Model Checker Safety Property Memory Module Arbitrary Waveform Generator Interactive Theorem Prover 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgement

Sandia National Laboratories is a multi-program laboratory managed and operated by Sandia Corporation, a wholly owned subsidiary of Lockheed Martin Corporation, for the U.S. Department of Energy’s National Nuclear Security Administration (NNSA) under contract DE-AC04-94AL85000. This work was funded by NNSA’s Advanced Simulation and Computing (ASC) Program.

References

  1. 1.
    Abadi, M., Lamport, L.: The existence of refinement mappings. Theoret. Comput. Sci. 82(2), 253–284 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  2. 2.
    Abadi, M., Lamport, L.: Conjoining specifications. ACM Trans. Program. Lang. Syst. 17(3), 507–535 (1995)CrossRefGoogle Scholar
  3. 3.
    Abadi, M., Merz, S.: On TLA as a logic. In: Proceedings of the NATO Advanced Study Institute on Deductive Program Design, pp. 235–271 (1996)Google Scholar
  4. 4.
    Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\(^ \text{+ } \) proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, pp. 44–44. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  5. 5.
    Cohen, E., Lamport, L.: Reduction in TLA. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 317–331. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  6. 6.
    The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)Google Scholar
  7. 7.
    Lamport, L.: The temporal logic of actions. ACM Trans. Program. Lang. Syst. 16(3), 872–923 (1994)CrossRefGoogle Scholar
  8. 8.
    Lamport, L.: Refinement in state-based formalisms. Technical report, DEC Systems Research Center (1996)Google Scholar
  9. 9.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)Google Scholar
  10. 10.
    Ricketts, D., Malecha, G., Alvarez, M.M., Gowda, V., Lerner, S. Towards verification of hybrid systems in a foundational proof assistant. In: MEMOCODE 2015, pp. 248–257. IEEE (2015)Google Scholar
  11. 11.
    Svenningsson, J., Axelsson, E.: Combining deep and shallow embedding for EDSL. In: Loidl, H.-W., Peña, R. (eds.) TFP 2012. LNCS, vol. 7829, pp. 21–36. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  12. 12.
    Wan, H., He, A., You, Z., Zhao, X.: Formal proof of a machine closed theorem in Coq. J. Appl. Math. 2014, 8 (2014). Article ID 892832, Hindawi Publishing Corporation, CairoMathSciNetGoogle Scholar
  13. 13.
    Wenzel, M.: The Isabelle/Isar Reference Manual (2012)Google Scholar
  14. 14.
    Yu, Y., Manolios, P., Lamport, L.: Model checking TLA\(^{+}\) specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999)CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG 2016

Authors and Affiliations

  • Philip Johnson-Freyd
    • 1
    Email author
  • Geoffrey C. Hulette
    • 2
  • Zena M. Ariola
    • 1
  1. 1.University of OregonEugeneUSA
  2. 2.Sandia National LaboratoriesLivermoreUSA

Personalised recommendations