Formal Methods and Theorem Provers

提供: T-VEC Wiki
移動: 案内検索

T-VECはフォーマルメソッド

フォーマルメソッドは、ソフトウェアおよびハードウェアシステムの仕様、開発、検証に用いることのできる、数学を基盤とした技術です。

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

T-VEC(定理証明として)- wikiの分類から

Level 2:定理証明によって、完全に機械的に証明が行われます。これは多くの費用を要するので、間違いによる損失が非常に高価である場合に、最良の実用価値を得ます(例えば、マイクロプロセッサ設計の重要な部分など)。

証明とテストについて

様々なタイプのフォーマルメソッドや、1つ以上のフォーマルメソッドをサポートする、様々なタイプのツールがあります。 しかしながら、全システム(航空電子、自動車、医療)を証明できる、フォーマルメソッド、またはツールはありません。一般に、定理証明を用いるそれらのフォーマルメソッドは、システムの限定された特性を証明することに適用されます。

TTMやSimulinkモデルは、T-VEC VGSによって証明される形式に変換されます(論理的な制約(logical constraints)DCP(Domain Convergence Paths (DCP))に一貫性があり、特定される入力ドメインに対する解を持つことの証明)。 そしてターゲットコードが、テストを通してDCPと、DCP上の制御と一致していることを証明するための、テストベクタを副産物として提供します。

モデルチェックによるテストのサポート

T-VEC VGS は、モデルチェックとテスト生成を行います。VGSは、全プログラムデータタイプとその操作(sin, cos, asin, acos, tan, ln, absなど多くのライブラリを含む)をサポートする定理証明のためのエンジンを、限られた目的を達成する為に用います。

その限られた目的とは:N個の変数と、一連の制約(constraints (precondition))に対し、各コンストレインツが満たされる、特定の変数セット(ある入力に対する出力の組合せ)を求めること

効果的なテストがT-VECによりできる理由は、事前条件の制約によって規定される、n次元スペースの極端なコーナーを攻めるデータ(テスト)を求めるからです。これらは、プログラムの欠陥を検出する可能性が高いポイント(テスト)です。

このコンストレインツ(制約)を解くプロセスは、モデルチェッキングでもあり、結果として、T-VEC VGSは、事前条件のコンストレインツ(制約)を満たすことができなければ、モデル上の欠陥(矛盾)として特定します。

一連のポイント(テスト)を求めると、VGSはその機能の期待値(postcondition)を算出します。そして、この期待値(postcondition)は、他の機能を参照し、そこで選択された範囲で満たされないことで矛盾となる可能性もあります。 このプロセスをより複雑にするのは、抽象化(submodels - procedures)の使用を必要とするコンストレインツの開発(またはモデル開発)、ですが、T-VECには一連のコンストレインツの階層化に対処するルールが備わっています。

標準について

IEC61508やISO26262は、フォーマルメソッドを推奨し始めています。

DO-178Bでは、やわらかい調子でフォーマルメソッドを議論ましたが、DO-178Cでは、より直接的に議論されています。