形式手法
形式手法(けいしきしゅほう、formal methods)
数学的に厳密に意味付けられた言語（形式仕様記述言語）を用いて情報システム（ソフトウェア、ハードウェア等）の要求や設計等を記述し、情報システムがユーザの要求等を満たしているかなど論理的に推論するための仕組みを提供する手法 要求や設計等を記述して、ユーザの要求等を満たしているかを確かめる手法
開発対象をより厳密に書き留め、解析可能にするための単なる「工学的」手法
ルールチェック付き仕様記述
要件定義、設計のときに役立つ技術。
ソフトウェアがある性質を満たしていることを論理的に検証するため、一定の不具合が存在しないことを保証できる。
分散技術の証明とかアルゴリズムの証明に使われる
銀の弾丸ではない、数学でもない(類似した記法は使う)
世界中で少しずつ採用が進んでいる
形式手法はテストを置き換えるものではない
仕様記述からコードを生成するツール
適用対象に応じて選択することが重要になる
理解度チェック
Q. 形式手法とは
Q. 形式仕様記述言語とは
Q. 形式的とは
Q. 何に使えるか
Q. ソフトウェア・テストとの違いは
Q. 形式手法の適用レベルとは
Q. 形式手法の適用レベル0
Q. 形式手法の適用レベル1
Q. 形式手法の適用レベル2
Q. 仕様
参考
2011/5/13
2012/11/15
2012年11月13日
関連
メモ