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

(→Proof versus Testing) |
|||

(One intermediate revision by one user not shown) | |||

Line 10: | Line 10: | ||

==Proof versus Testing== | ==Proof versus Testing== | ||

− | There are | + | 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 [[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. | |

− | T-VEC | + | |

− | + | ===Model Checking Supports Testing=== | |

+ | T-VEC VGS is for model checking and test generation. VGS 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.). | ||

− | What makes T-VEC | + | :The simple goal is: given a set of n variables, and a set of constraints (precondition), find a set of data point for the variables, such that each constraint is satisfied. |

+ | |||

+ | What makes T-VEC effective for testing is that it finds the data (test) points at the extreme corners of the n-dimensional space defined by the constraints of the precondition. These are points that are more likely to expose program faults. | ||

+ | |||

+ | :This constraint solving process is also a form of model checking, and as a result the T-VEC VGS may also identify model faults (contradictions) when it cannot satisfy the constraints of a precondition. | ||

+ | Once it finds a set of points, it attempts to compute an expected output for the function (postcondition), which can also have contradictions through references to other functions that cannot be satisfied by the selected set of points. What further complicates the process is that constraint development (or model development) requires the use of abstraction (submodels - procedures), and T-VEC has rules to deal with hierarchies of constraint sets. | ||

==Standards== | ==Standards== |

## Latest revision as of 13:30, 15 February 2007

T-VEC is a formal method.

Formal methods are mathematically-based techniques for the specification, development and verification of software and hardware systems.

See http://en.wikipedia.org/wiki/Formal_methods

T-VEC (behind the scenes is a Theorem Prover) - per the wiki taxonomy

Level 2: Theorem provers may be used to undertake fully formal machine-checked proofs. This can be very expensive and is only practically worthwhile if the cost of mistakes is extremely high (e.g., in critical parts of microprocessor design).

## Proof versus Testing

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 (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

T-VEC VGS is for model checking and test generation. VGS 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.).

- The simple goal is: given a set of n variables, and a set of constraints (precondition), find a set of data point for the variables, such that each constraint is satisfied.

What makes T-VEC effective for testing is that it finds the data (test) points at the extreme corners of the n-dimensional space defined by the constraints of the precondition. These are points that are more likely to expose program faults.

- This constraint solving process is also a form of model checking, and as a result the T-VEC VGS may also identify model faults (contradictions) when it cannot satisfy the constraints of a precondition.

Once it finds a set of points, it attempts to compute an expected output for the function (postcondition), which can also have contradictions through references to other functions that cannot be satisfied by the selected set of points. What further complicates the process is that constraint development (or model development) requires the use of abstraction (submodels - procedures), and T-VEC has rules to deal with hierarchies of constraint sets.

## Standards

IEC61508, ISO26262 have been started to recommend Formal Method.

DO-178B discusses formal methods in a "soft" tone, but DO-178C is discussing it more directly.