Publications Details

Demonstration of Model-Based Design for Digital Controller Using Formal Methods

Mayo, Jackson R.; Morris Wright, Karla V.; Aytac, Jon M.; Smith, Andrew M.; Armstrong, Robert C.; Hulette, Geoffrey C.; Lober, Randall R.

This report describes work originally performed in FY19 that assembled a workflow enabling formal verification of high-consequence digital controllers. The approach builds on an engineering analysis strategy using multiple abstraction levels (Model-Based Design) and performs exhaustive formal analysis of appropriate levels – here, state machines and C code – to assure always/never properties of digital logic that cannot be verified by testing alone. The operation of the workflow is illustrated using example models and code, including expected failures of verification when properties are violated.