FreeStyleWiki

形式仕様言語

[数学,形式検証]

形式仕様言語

  形式検証入門

形式検証(Formal Verification)
  • Formalは形式と訳すが,記号的にとか,堅苦しいという意味もある.
  • 要するに記号化したもの(例えばプログラム)を対象に,記号に基づいて検証を行う.
古典的なテストは「未知」に弱い
  • 人間がテストケースを与える
    • 明示した有限個のケースしか保証できない
    • 思いつかない異常系はそもそも考慮外
形式手法とは
  • システムを数学的対象により表現
    • その対象の性質に基づいて検証を行う
    • 対象として何を選ぶかでツールの性質が決まる
    • テストケースの抜けや漏れが生じない
形式手法の分類
  • モデル検査
    • システムが取りうる値を列挙して探索
    • 有限個のパターンに収まれば自動化できる
  • 定理証明
    • いわゆる数学的な証明をプログラム的に表現
    • 真に無限個のパターンを扱うことができる

というわけでモデル検査をやりたい

  モデル検査概説

  • モデル検査手法:考えられる状態をすべて自動的に探索する
    • 有限状態で特徴づけられるプロセスの並行動作にまつわる性質など。
    • 代表的なツール:NuSMV, Spin, LTSA, UPPAAL, etc.
  • モデル検査の「モデル」≠UMLなどの「モデル」
    • 論理学では、与えられた性質をp、対象となる振る舞いをMとすると、「Mに対してpが成立する」ことを、「Mはpのモデル」であると呼ぶ。
    • モデル検査:振る舞いが記述した性質のモデルであることを検査する

  定理証明概説

  • 定理証明手法:対話的に証明する。部分的に自動化を行う、適用対象は以下の通り
    • 述語論理で書かれた式の正しさなど。
      • \( \forall x y, x \le y \land y \le x \Rightarrow x=y, \forall n (n \cdot (n+1)) mod 2 = 0 \)
    • 算術計算など、いろいろなデータ型や演算を含む事実を証明することは決定不能問題だから
      • 決定不能問題:問題を解くアルゴリズムが存在しない(すなわち、自動的に問題が解けない)