Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki
Jump to: navigation, search
(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 [[Domain Convergence Paths|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.
+
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===

Latest revision as of 12:30, 15 February 2007