形式手法の使い道

形式手法はブレイクするはずとずっと言われながら、なかなか普及しない。
その理由は形式手法の使い道が限られているからだと思っている。
考えたことをメモ書き。

形式手法は各種の手法があるが、モデル検査が一番わかりやすい。
モデル検査のやり方は、実際のプログラムから状態遷移図というモデルをリバースして、本来の仕様と状態遷移図を比較検討して、ありえない状態遷移があればそれはバグになることを説明するのに使う事例が多い。

モデル検査の分かりやすい例としては、以前出題されたソフトウェア開発技術者試験の午後問題があげられる。
下記の問題2に相当する。

平成20年度春期試験ソフトウェア開発技術者試験（SW）午後Ⅰ

問題では、ある関数のフローチャートから状態遷移図を生成する。
その状態遷移図に対して、不具合を発見するために、不具合が存在しない条件式つまり本来の仕様を定義した後、モデル検査ツールを使って状態遷移図を網羅的にチェックして、条件式を満足するかどうか判定する。
当然、条件式を満たさない場合、バグになる。
そのバグは、モデル検査ツールが状態遷移図の経路に相当するので、不具合を再現する事が可能になるという流れ。

上記の問題にも書かれているが、モデル検査の特徴はいくつかある。
一つは、従来のテストのように大量のテストデータを準備する必要はない。
状態遷移図さえモデル化できれば、モデル検査ツールを使って、すべての経路計算をすればいい。
ソフトウェアテストが難しい理由の一つは、多種多様なテストデータの作り込みに手間がかかることだから。

もう一つは、再現しづらいバグや複雑な仕様の組みわせで発生するバグを発見しやすいこと。
この種類のバグは、探索的テストで発見する時が多いが、限られた工数で探索的テストを実施して、非常に稀だが重大なバグを発見できるとは限らない。
むしろ、モデル検査ツールを使って、総当たりで自動計算した方が効率が良い場合もある。

だが、モデル検査ツールは既存のプログラムから状態遷移図を自動生成してくれるとは限らない。
そもそもシステムの状態遷移図をきちんと作るのはかなりの技術力を要するし、労力もかかる。
また作成した状態遷移図の精度が高くなければ、当初の目的である再現しづらいバグを見つけることができない。
もちろん、状態の数が多いほど計算は爆発するので、いくらコンピュータの性能が良くなったと言っても、すべての状態の経路を計算し尽くすことができない場合もある。

このように、形式手法の1種類であるモデル検査の使い道は、ソフトウェアテストの中でも探索的テストを補完するような使い道しかない。
信頼性が品質要件で非常に重要なプロジェクト、例えば人工衛星や社会的インフラの場合では、モデル検査による再現しづらい不具合探しも重要だろう。
だが、ソフトウェアテストの本質的な問題に焦点を当てているとはいえないと思う。

形式手法はもちろんこのような使い道だけではない。
形式手法の本来の使い方は、プログラミングに入る前の設計工程で、SEが作った詳細な設計書に書かれた仕様を形式手法でモデル化して、矛盾や不整合を洗い出すことにある。
IPAが組込ソフトウェア開発の品質改善で形式手法を適用できないか、長年研究している理由はそこにある。
しかし、そのやり方はまだうまくいっているとは言えないと思う。

また、この発想はウォーターフォール型開発特有の考え方だ。
何故なら、前工程の手戻り作業をできるだけなくすために、プログラミングせずに設計工程の品質をあげようとするやり方だから。
この発想は、ソフトウェア開発を工程単位に分断せず、設計もプログラミングもテストも一体化して開発を進めるアジャイル開発とは本質的に異なる。

とはいえ、形式手法とアジャイル開発を組み合わせて実践されている細谷さんの事例もある。
色々探ってみる。