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

From T-VEC Wiki

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.). | ||