Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki
Jump to: navigation, search
Line 12: Line 12:
 
There are many many types of "formal methods" and many types of tools that support one or more types of formal methods. However, is not likely that there is a formal methods or tools that can "prove the whole (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 level. TTM/Simulink/T-VEC "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.
 
There are many many types of "formal methods" and many types of tools that support one or more types of formal methods. However, is not likely that there is a formal methods or tools that can "prove the whole (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 level. TTM/Simulink/T-VEC "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.
  
===Simple Proof Supporting Testing==
+
===Simple Proof Supporting Testing===
 
T-VEC is for test generation and uses a theorem proving engine with a few simple goals that are implemented in rules covering all program data types and operations, including many library operations (e.g., sin, cos, asin, acos, tan, ln, abs, etc.).  
 
T-VEC is for test generation and uses a theorem proving engine with a few simple goals that are implemented in rules covering all program data types and operations, including many library operations (e.g., sin, cos, asin, acos, tan, ln, abs, etc.).  
  

Revision as of 10:14, 15 February 2007