テストの本質を探る　――30年の歴史を持つ 「ソフトウェア工学」の知恵に学ぶ

●○●　Column　●○●
◆V&Vのいろいろ-2◆

●形式的手法：LSI検証の分野で実用化

　次に紹介するのは形式的な方法です（表C-2）．ここでいう「形式的な（formal）」というのは，それがなんらかの数学的なモデルに基づいて記述されているということを意味しています．正しくなんらかの数学的モデルに基づいていれば，機械的に検証することも可能となります．数学的モデルとしては，公理的集合論や述語論理などが用いられます．

　形式的検証の場合，テスト・ケースを実行するための入力ベクトルを用意する必要がありません．例えば，y＝x²であるとき，xに1や－1を入れてみてyがどうなるかを試してみなくても，（例えば）y≧0は数学的に明らかです．その意味で，先の「非形式的な方法」をまとめて動かして結果をみるという意味で「シミュレーション」と呼ぶ場合もあります．

　残念ながらソフトウェア開発の現場で，形式的検証が用いられることはほとんどありません．ソフトウェアが対象とする多くのものは人間系であり，例えば使い勝手にかかわるようなもの（画面全体の色調を明るく，など）は，数学的に表現することが困難です．また，結果がほんとうに正しいかどうかは人間にしかわかりません．

　もちろん，人間系が介在しない世界（通信プロトコルの実現）や，総合的に人間が介在するにしても，人間の生命にかかわるような領域（よくある例は，踏み切りのシステム）では有効な手段になります．また，LSI設計の世界ではかなりポピュラな手法になってきています．

　V&Vは，決まったルールに従う標準化のようなものと思われるかもしれません．最後は具体的なものに対する個別の議論になります．プロジェクトは，QCD（品質，コスト，デリバリ）の制約をつねに受けます．その中で，必要に応じて（それが，形式的であろうと非形式的であろうと）採用するということになります．重要なことは，場面に応じてどのV&Vが使えるかを知っていること，ということになります．

〔表C-2〕形式的なV&Vの方法
リアルタイム・プロパティとは，一般に「活性（liveness；望んでいることはいつかは生じる）」と「安全性（safety；望んでいないことは決して起こらない）」を指す．