形式手法・ツール分類

このページでは,代表的な形式手法・ツール,それらの分類について述べます.ここまで「ポイント」として挙げた「モデル化・記述の対象および抽象度」,「検証の対象と方法」の異なる様々な手法・ツールが存在します.

本サイトでは,様々な形式手法・ツールの位置づけのポイントとして,以下の二点を挙げてきました.

また実際には,これらの観点を踏まえ,「開発プロセスの中でどう位置づけ活用していくか?」ということが問題となってきます.

以下では,形式手法・ツールの分類について説明します.ここではよく用いられる分類(カテゴリ名)を挙げ,簡単に個々の特徴について述べます.ただし,分類の観点というのは複数ありますし,また分類は多くの場合排他的でなく「どっちとも見なせるもの」「組み合わせたもの」があります.このため以下に挙げるものが「絶対的な」「万人共通の」分類というわけではありません.

モデル検査: 設計の網羅的な検証

ポイント(2): 検証」ページで説明したように,「モデル検査」という言葉は検証方法の名称です.システム内の複雑な状態遷移に焦点を絞って,実行の順序や分岐の可能性を網羅的に検査し,期待された性質が成り立つかどうかを検証する方法を指します.人手やテスティングでは検出できない潜在的な誤りを見つけることができるため,「複雑な設計の正しさを保証したい」際によく用いられます.

このように「モデル検査」という言葉は元々「検証方法」の名称ですが,形式手法・ツールの分類名として用いられることも非常に多く,その場合はSPINやLTSAなどモデル検査に特化した専用ツールを指します.

「モデル検査」に分類される手法・ツールは以下のような特徴を持ちます.

  • 「システムの状態がどのように変化する可能性があるか」に関するモデルを与え,「デッドロックしない」「いつか必ずこの状態に達する」といった,実行の経過に関する性質を検証する.
  • ある定義された範囲に対し,網羅的な検査を行う.テストケースを定める必要がなく,また与えた範囲内で漏れのない検査を行うことができる.このため,設計の完全・網羅的な検証を目的として用いられる.
  • スレッド間の排他制御・同期制御やネットワークプロトコルなど,実行の分岐・順序の可能性が複雑な部分の検証に利用される.
  • システムの中で特に複雑な部分にピンポイント絞って利用することができる.逆に,網羅的な検証を可能とするため,扱う部分を限定して,検証のための抽象的なモデルを別途構築する必要がある.
  • SPIN,LTSA,SMV,UPPAALなどのツールが知られている.
  • 「実行にかかる時間や,それに関する性質(デッドラインなど)」,つまり実時間性(リアルタイム性)を扱うかどうかにより,ノウハウやツールに求められる機能が大きく変わってくる.実時間性を扱う手法・ツール(UPPAALなど)は,「実時間モデル検査」などと呼ばれる.

形式仕様記述: 要求からプログラムに至る過程を明確化・厳密化

自然言語による要求記述から最終的なプログラムに至るまでの過程では,要求・仕様や設計に関する成果物が生み出されていきます.その過程では,「何をするか(what)」という情報から「どう実現するか(how)」という情報が順次定められ,詳細化されていくこととなります.各過程の成果物であるに対しては,様々な分析・検証作業が考えられます.また,詳細化において前段階の成果物(モデル)が正しく反映されているかということの検証も必要となります.

このように,プログラムにつながる途中過程の成果物を明確化・厳密化し,分析・検証を行うための形式手法・ツールは形式仕様記述と呼ばれます.

「形式仕様記述」に分類される手法・ツールは以下のような特徴を持ちます.

  • 開発プロセスのどの段階を対象としているのかにより,記法,特に抽象度はまちまちである.また,想定している分析・検証も手法・ツールにより多種多様である.求められる性質の完全な検証を想定する場合定理証明を考えることが多い.一方で,より手軽な分析・検証として,シミュレーションによる動作確認,テスティングによる検証,(GUIを伴う)プロトタイピングによる妥当性確認を考えるものもある.
  • プログラムの構造に近い形で,変数によるシステム状態の表現と,それらを読み書きする操作を記述する手法・ツールは,モデル指向形式仕様記述と呼ばれる.VDM,B,Z,Alloyなどが知られている.オブジェクト指向に基づいたモデル化・記述を行うなど,JavaやC++による実装につないでいく手法・ツールも多い.
  • 変数や関数・操作の詳細よりも,より抽象的にシステムの機能を数式に近い形で書き表す手法・ツールは,性質指向形式仕様記述と呼ばれる.OBJ,CafeOBJ,LOTOSなどが知られている.
  • 数式のような形式で,コンポーネントとそれらの間のメッセージ送受信を抽象的に記述する方式はプロセス代数と呼ばれる.プロセス代数に基づいた形式仕様記述としては,CSPが代表的である.
  • ある段階の成果物であるモデルとそこから導かれたより詳細なモデルとの対応づけ(詳細化),およびその検証を考えることが多い.ここで詳細化としては,ブラックボックスとして定義していたシステムのサブシステムへの分割や,「何をするか」が抽象的に定められた関数・操作における「どう実現するか」のより詳細の決定などが挙げられる.

プログラム検証: 最終的な実装の検証

モデル検査にしろ,形式仕様記述にしろ,実際に詳細なプログラムを作ってしまう前に,理解を深め誤りを取り除いておくという思想に基づいています.これは,要求や設計における誤解や誤りが実装やテストの段階になってようやく発覚する場合,手戻りのコストが非常に大きくなってしまうためです.このように形式手法・ツールでは,開発の早い段階での成果物の質をその時点で確認し高めておくことを考えます.つまり,そのためには,開発の早い段階により大きなコストをかけ,それを後ろの段階での大きなコスト削減につなげていくことを考えます.しかしこの思想を実現しようとすると,既存の開発プロセスをそれなりに変える必要が出てきます.これまでとは人月等の見積もりも変わってくるでしょう.また,最終的には,仕様や設計が正しくとも,システムの実装であるプログラムに反映されていなければ意味がないので,実装の検証は重要な意味を持ちます.

このため,形式手法・ツールにおける検証方式を実装・テスト段階において活用しようという考え方があります.テスティングの補完・強化としてより手軽に,形式・手法ツールの恩恵を受けようとするものです.本サイトではそのような手法・ツールをプログラム検証と呼びます.

「プログラム検証」に分類される手法・ツールは以下のような特徴を持ちます.

  • Cなどで書かれたプログラムに対して,成り立つべき性質を明示化し,検証を行う.検証の方法としては,「実行・観測」による検証が主となる.実行・テスティングの際に,与えられた性質を検証する動作を挟みながら実行を進めるものがある.またより強力な検証として,プログラムのうち関連する文のみを抜き出し,決められたステップ数などで網羅的に分岐を調べる有界モデル検査が注目されている.
  • プログラムは非常に詳細で複雑なので,完全な検証は難しい.
  • 検証対象となる性質としては,モデル指向形式仕様記述で扱うような,変数の値が満たすべき条件や,関数・メソッドの前提条件や実行後の効果に関するものが主となる.
  • プログラム固有の問題として,ポインタやメモリの管理に関する性質を扱うツールもある.
  • JML,Java PathFinder,CMBC,VARVELなどのツールがよく知られている.

このページの先頭へ戻る