前に、聞かれて、答えたことを、忘れないうちにメモメモ
要求仕様の全てを、ある形式仕様言語で確認するというのは、不可能でないかもしれないけど、
難しい。
ここで、要求仕様を
・機能要件
概念モデルとユースケース
・非機能要件
性能
信頼性
ユーザビリティ
とわけると、機能要件に関しては、形式仕様言語（ＶＤＭとかＢとかＺとか）で確認できるけど、
非機能要件に関しては、得意ではない。
性能に関しては（何分以内で帰ってくる）出来ないことはないけど、あまり得意ではないし、
信頼性も・・・ユーザビリティにいたっては、形式仕様言語で確認したいなら、まず
ユーザビリティとは何か？から定義しないといけないので、実質、これはできない。
性能に関しては、モデル検査のほうが適している。
■機能要件と形式仕様言語
機能要件に関して、機能は、概要的なものから、詳細的なものまで、レベル化されている。
このうち、あるレベルにおける全体の整合性、一貫性を確かめるということと、
上位レベルと下位レベルの整合性(詳細化）を確認するという２つの話がある。
ＶＤＭは、基本的に、全体の整合性、一貫性を調べるのに向いている。
そして、これは数学的に証明するのではなく、データをいれて確認する。
要するに、仕様をデータでテストしているイメージ。
なので、数学的な確からしさは？だけど、実装のときと同じテストデータを使うこともできるので
工程における一貫性を担保することができる。
数学的に確かであるということを証明するのはＢメソッド。
また、Ｚは、数学的に確かなことも、データを入れて確認することも出来る。
Ｂを拡張したＥｖｅｎｔ－Ｂは極め付けで、
・数学的な確からしさで、同一レベルの整合性を確かめることも出来るし
・数学的な確からしさで、詳細化のチェックも出来るし
・データをいれて、振る舞いを確かめるＶＤＭみたいなこともできる
ただし、その分、ＢもＥｖｅｎｔ－Ｂも、数学的に正しいことを証明するのが、結構面倒で、ツールが自動証明してくれるんだけど、その証明に失敗した場合、仕様が間違ってるのか、自動で証明できないだけなのかがわかりにくい（少なくとも初心者は）。
実装に近い形式仕様としては、ＪＭＬやＥＳＣ／Ｊａｖａ２などがある。
■非機能要件とモデル検査
非機能要件に関して、そもそも、並列条件において、デットロックが起きないかというようなことを形式仕様で調べるには、ちょっとたいへん。そのような拡張は出来るかもしれないけど、全部調べるとなると、いろいろなケースがありすぎて（状態爆発）、調べきれない。
そこで、そのような並列処理におけるデッドロックとかを調べるものとして、モデル検査がある。
ＳＰＩＮ，ＳＭＶ、ＬＴＳＡなどが挙げられる。これらは、デッドロックとかを調べられる（さまざまなケースを想定してチェックしていく）。
ＦＤＲ（プロセス代数ＣＳＰのモデル検査）や、ＪＣＳＰ（そのＪａｖａ版）もそうだけど、ＣＳＰの場合、イベントの振る舞いが隠蔽されているかどうかという観点からの詳細化も確認できる。
ただ、時間的な性能に関しては、ＵＰＰＡＡＬが使われる。
ユーザビリティに関しては、これらでは確認できず、実装してみるしかない。
アクセス
トータル
ランキング
