# Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki

(→Proof versus Testing) |
|||

Line 12: | Line 12: | ||

There are many types of "formal methods" and many types of tools that support one or more types of formal methods. It is not likely that there is a formal method or tool that can "prove an entire (avionics, automotive, medical) system." Those formal methods that use theorem provers are generally applied to proving specific properties about a system, usually from an abstract point-of-view. | There are many types of "formal methods" and many types of tools that support one or more types of formal methods. It is not likely that there is a formal method or tool that can "prove an entire (avionics, automotive, medical) system." Those formal methods that use theorem provers are generally applied to proving specific properties about a system, usually from an abstract point-of-view. | ||

− | TTM or Simulink models are translated into a form where the T-VEC VGS "proves" that the logical constraints of a [[ | + | TTM or Simulink models are translated into a form where the T-VEC VGS "proves" that the logical constraints of a [[Modeling#Model Representation|Domain Convergence Paths (DCP)]] are consistent and have a solution in the specified input domain. It then provides a test vector as a byproduct that can be used to "demonstrate" through testing that the target code is consistent with the DCP and the computation that the DCP controls. |

===Model Checking Supports Testing=== | ===Model Checking Supports Testing=== |