| モデル検査に関するＱ＆Ａ |
| [Q.10] ソフトウェア開発工程におけるモデル検査の費用対効果について定量的なデータはありますか？ |
モデル検査の所用時間としては、2004年に実施した設計仕様書のモデル検査が160時間を要し(*1)、昨年に実施したデバッグへの適用では20時間で不具合を見つけることができました(*2)。
再現性の低い不具合のデバッグでは、モデル検査は、コードレビューよりも明らかに費用対効果が高くなります。しかし、設計仕様書のモデル検査では、発見されたバグの評価が難しく、費用対効果を定量的に表すに至っていません。同種ソフトウェアの開発が繰り返されていれば、工程実験により費用対効果を求めることも可能ですが、これまでの適用事例は全て単品システムであり比較対象がありませんでした。
今後、良いデータが得られれば発表して行きたいと考えています。 |
|
| (*1) 「モデル検査のデバッグへの適用とモデル化作業支援」JaSST'06 in 大阪 |
| (*2) 「組込みソフトウェア開発のイン-デザイン モデル検査」JaSST'04 |
|
|
| [Q.9] モデル検査の結果で、システムにバグのないことを証明できるのですか？ |
モデル化した範囲・レベル（詳細さ）・検査項目の範囲では、バグがあれば必ず検出することができます。
しかし、その範囲の外側を検査することはできません。
そのため、不具合が予想される要素がモデル化の際に抜け落ちないように注意が必要です。 |
|
|
| [Q.8] 対象システムの全ての状態遷移をモデル検査言語により書き直すとすると、その作業は大変ではないでしょうか？ |
確かに、モデル検査言語によるプログラム作成の作業時間は必要です。
しかし、対象システム全体の状態遷移を１枚の大きな状態遷移図に書いてからモデル検査言語を使って書き直す訳ではなく、対象システムの変数１つ１つに着目した小さな状態遷移図をモデル検査言語で記述して入力プログラムとして繋げれば、全体の状態遷移図はモデル検査器の中で自動的に合成されます。 |
|
|
| [Q.7] モデル検査では、負荷テストのようなことはできないのでしょうか？ |
| 実システムを稼動させる検査ではありませんので、負荷テストはできません。 |
|
|
| [Q.6] モデル検査により検出された不具合が、実システムにも存在していることは、なぜ判るのでしょうか？ |
確かに、モデル検査器から得られた結果は、モデルに存在しているだけです。
その内容を読み取って、同じ間違いが実システムに存在しているかどうかを確認するのは、人間の仕事になります。
モデル検査器の出力には、モデル化の誤りや、検査項目の誤りによりるものも含まれているため、内容を確認して、実システムの不具合だけを見つけ出す作業が必要です。
ただし、モデルの元となった実システムの仕様を理解していれば、検出された不具合が実システムに存在するか否かは比較的簡単にわかります。 |
|
|
| [Q.5] システム全体を最初から開発する場合には、モデル検査の導入が容易だと思いますが、既存システムを改良する場合には、導入が難しいように思いますが？ |
システム全体をモデル検査するためには、既存部分のモデル化が必要であり、そのための手間が発生することは止むを得ません。
一旦、モデルを作成するとシステムの改良に合わせてモデルを改良・再利用できるメリットがありますが、最初のモデル化の手間を省略できる都合の良い方法はありません。
期待する検査項目にも関係しますが、既存部分の抽象度を高くするか、非決定性を使ってモデル化記述を簡単にする工夫はできると思います。
システム全体に適用することを断念した場合でも、デバッグでモデル検査を使う方法は、利用可能で有効です。もちろんその外部入力が変化した場合の応答をモデルに記述しておく必要があります。 |
|
|
| [Q.4] モデル検査を実務に適用する際に、最も注意すべきことは何でしょうか？ |
見方によっては違う答えがあるかも知れませんが、検査対象を良く理解することと、価値のある検査項目を設定することが大切だと考えています。
どちらもモデル検査そのものの知識ではありませんが、検査あるいは現場運用で問題になる要素を漏れなく取り込んだ適切なモデルを作成しなければ、有効な検査が出来ません。
従って、検査対象をよく理解するために設計者の協力を得ることが必要になります。 |
|
|
| [Q.3] 何時変化するかわからない外部要因があるのですが、モデル検査で扱えますか？ |
| 非決定性の外部入力として考えて処理します。もちろんその外部入力が変化した場合の応答をモデルに記述しておく必要があります。 |
|
|
| [Q.2] モデルが大き過ぎて、一度にモデル検査できない場合は、どのようにして扱うのですか？ |
| 我々の場合は、モデルをモジュールに分割して、モジュール単位のモデル検査を行い、さらに機能別に複数のモジュールを組み合わせたモデル検査を行いました。 |
|
|
| [Q.1] モデル検査器から現実的でない不具合が数多く出力されて困っています。改善できないでしょうか？ |
モデル検査の精度を上げようとして詳細なモデルを作成すると、出力されるFalseの数は多くなる傾向があります。
出力された反例を見て、その条件の発生頻度や影響の大きさを検討した結果、現実的でないと判定される場合も増えてきます。
もちろん、モデルを荒くすることで出力されるFalseの数を減らすことが出来ますが、重要な問題を見えなくする危険性があるため、数だけを考えてモデルを荒くすることはお薦めできません。
反例の内容をよく検討した上で、検査項目やモデルの変更を行う必要があります。 |
|
|
|
