形式手法あれこれ

形式手法(Formal Method)と言われる分野にはおおざっぱに分けて形式仕様記述とモデル検査がある。それから、形式的開発手法というか開発プロセス的にまとめたものがある。

形式仕様記述ではVDM, Z等が有名である。モデル検査ではSPIN, NuSMV等が有名である。形式的開発手法にはB-method,RAISE等がありどれが有名と言うことはない。

VDMはツールの名前でもあるし言語の名前、あるいは記述スタイルを指して使われるが、Zは言語あるいは記法であり適当な専用ツールが無い。Zは好きだけど動かないからVDMを使う人は多い。それじゃZは使えないかと言うと事例はある。日本では使うの使わねぇのと言う段階から使えるのか使えないのかと言う議論が始まるまでに10年掛かったが、海外には成功事例も失敗事例もちゃんとある。

Zは集合論とλ計算など数学とコンピュータサイエンスの合わせ技で構成されている。形式的開発手法の中にも機能要求、非機能要求、動作要求を記述するためにCSP等のプロセス代数を組み合わせたものがある。組み合わせとしてはVDM/CSP/DC(Duration Calculus)が一番多いかも知れない。DCはインターバルロジックと言うこともある。

業務系だとVDMやZあるいは定理証明のCoq等が使われる。定理証明系のツールは難しいのでだんだん使われなくなっているとも聞く。例えばマスターカードなど。定理証明を使うよりモデル検査と組み合わせる方が楽かも知れない。

組込系だと動きの記述が重要になるのでプロセス代数系の手法が重要である。インターバルロジックも重要だがツールや適用事例をあまり聞かない。これからなのかも知れない。DCについては昔インタフェースに記事を書いたことがある。

組み込みソフトへの数理的アプローチ（第1回）時間仕様のあつかいガス・バーナー問題の例