書いたっけ？ま、一応書いておく
形式仕様には、形式仕様記述とモデル検査が大きく分けるとある。
形式仕様記述は、自動証明とか使うと、正確さの面では、完璧に見えるかもしれない。
たしかに、機能要件的には完璧になるかもしれないが、自動証明は、数学的に証明できないものには、効果はない。
たとえば、足し算の性質が成り立つ、つまり１＋１＝２に必ず成ってくれるのであれば、足し算に関する証明はできるかもしれない。しかし、前提部分が成立しない、１＋１＝１に成ってしまうような、並列処理で排他制御してないような状況で、証明が成り立ったからって、かならずしも、全ての状況で正確な答えを出すとは限らない。
また、停止性の問題がある。停止しないものは証明できない。デッドロックになったり、無限ループを起こす証明は出来ない。
つまり、演繹的に正当性を証明する、形式仕様記述には限界がある。
このような点を補完するものに、モデル検査がある。モデル検査は、しらみつぶしにケースをつぶしていく。帰納的に正当性を証明するかんじ。
これなら、たとえば、ＳＰＩＮでデッドロックを示したりすることは出来る。排他制御などの検証もできる。ＬＴＬ式で記述できるような内容は、確かめられる。
時間的なものは苦手だけど、それは、Uppaalだとできる。
ということで、性能とか、非機能要件の一部は、モデル検査でできる。
しかし、これらは、シミュレーションをするに過ぎない。シミュレーションは、調べたい概念について調べるのであって、想定の範囲外のものについて、調査はできない。
それらは、実機でテストするしかない。
ということで、形式仕様記述、モデル検査、実機テストすべて必要になる。
形式仕様には、形式仕様記述とモデル検査が大きく分けるとある。
形式仕様記述は、自動証明とか使うと、正確さの面では、完璧に見えるかもしれない。
たしかに、機能要件的には完璧になるかもしれないが、自動証明は、数学的に証明できないものには、効果はない。
たとえば、足し算の性質が成り立つ、つまり１＋１＝２に必ず成ってくれるのであれば、足し算に関する証明はできるかもしれない。しかし、前提部分が成立しない、１＋１＝１に成ってしまうような、並列処理で排他制御してないような状況で、証明が成り立ったからって、かならずしも、全ての状況で正確な答えを出すとは限らない。
また、停止性の問題がある。停止しないものは証明できない。デッドロックになったり、無限ループを起こす証明は出来ない。
つまり、演繹的に正当性を証明する、形式仕様記述には限界がある。
このような点を補完するものに、モデル検査がある。モデル検査は、しらみつぶしにケースをつぶしていく。帰納的に正当性を証明するかんじ。
これなら、たとえば、ＳＰＩＮでデッドロックを示したりすることは出来る。排他制御などの検証もできる。ＬＴＬ式で記述できるような内容は、確かめられる。
時間的なものは苦手だけど、それは、Uppaalだとできる。
ということで、性能とか、非機能要件の一部は、モデル検査でできる。
しかし、これらは、シミュレーションをするに過ぎない。シミュレーションは、調べたい概念について調べるのであって、想定の範囲外のものについて、調査はできない。
それらは、実機でテストするしかない。
ということで、形式仕様記述、モデル検査、実機テストすべて必要になる。
アクセス
トータル
ランキング
