Verification by Way of Refinement: A Case Study in the Use of Coq and TLA in the Design of a Safety Critical System
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.
KeywordsModel Checker Safety Property Memory Module Arbitrary Waveform Generator Interactive Theorem Prover
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.
- 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
- 6.The Coq Development Team: The Coq proof assistant reference manual. LogiCal Project, Version 8.0 (2004)Google Scholar
- 8.Lamport, L.: Refinement in state-based formalisms. Technical report, DEC Systems Research Center (1996)Google Scholar
- 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.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
- 13.Wenzel, M.: The Isabelle/Isar Reference Manual (2012)Google Scholar