形式仕様言語
- このページは以下の資料を元にスクラップブックのようにまとめている
形式検証入門
- 形式検証(Formal Verification)
- Formalは形式と訳すが，記号的にとか，堅苦しいという意味もある．
- 要するに記号化したもの（例えばプログラム）を対象に，記号に基づいて検証を行う．
- 古典的なテストは「未知」に弱い
- 人間がテストケースを与える
- 明示した有限個のケースしか保証できない
- 思いつかない異常系はそもそも考慮外
- 形式手法とは
- システムを数学的対象により表現
- その対象の性質に基づいて検証を行う
- 対象として何を選ぶかでツールの性質が決まる
- テストケースの抜けや漏れが生じない
- 形式手法の分類
- モデル検査
- システムが取りうる値を列挙して探索
- 有限個のパターンに収まれば自動化できる
- 定理証明
- いわゆる数学的な証明をプログラム的に表現
- 真に無限個のパターンを扱うことができる
というわけでモデル検査をやりたい
モデル検査概説
- モデル検査の「モデル」≠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 \)
- 算術計算など、いろいろなデータ型や演算を含む事実を証明することは決定不能問題だから
- 決定不能問題：問題を解くアルゴリズムが存在しない（すなわち、自動的に問題が解けない）
- 述語論理で書かれた式の正しさなど。