Difference between revisions of "Formal Methods and Theorem Provers"

From T-VEC Wiki
Jump to: navigation, search
 
Line 8: Line 8:
  
 
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).
 
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).
 +
 +
===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.

Revision as of 11:58, 14 January 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).

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.