Sandia_Natl_Labs_FY19_LDRD_Annual_SAND2020-3752 R_2_S

FY19 ANNUAL REPORT

A domain-specific language for high-consequence control software. Formal methods approach the verification of digital systems using the mathematics by which, and for which, they are created—

formal logic. This approach is particularly valuable for the design and verification of embedded digital systems in high-consequence control systems such as nuclear weapons. Under a Sandia LDRD, a formal specification language was developed and implemented within the Q formal verification toolset. The formal semantics enables machine-checked proofs of key properties, including real-time functionality, and correct-by-construction techniques important to affirming the safety, security, and reliability of the device. This capability is now being successfully applied within the Nuclear Deterrence program generally, and current life extension programs specifically. Example of a formal specification using the language developed through the LDRD. (Image courtesy Robert Armstrong)

25

LABORATORY DIRECTED RESEARCH & DEVELOPMENT