論文：複数のユースケース記述に対するモデル検査を用いた要求検証プロセスの提案
本日はこちら。
形式手法による要求の検証のようですね。
まとめると、
・モデル検査により要求を検証する方法は確立されているとは言えない
・ユースケース記述に対してモデル検査をかけて、要求の矛盾を見つける
・数個のユースケース記述で評価し、欠陥が見つけられた
ということです。
例のごとく、気になる箇所を引用していきます。
要求を表現したユースケース記述を状態遷移モデル化し、モデル検査で検証する試みがなされている
そうなんですね、とても気になります。読みます。モデル検査そのものを見ていると、設計モデルとかのレベルでの議論が多い気がしていて、要求で使えるのかについては大いに興味があります。
複数のユースケース記述を状態遷移モデルに変換して一度に検証するのではなく、まず要求を小さく分割した各ユースケース記述の単位で検証する
ボトムアップというか、細かい単位での検証を積み上げるんですかね。考え方自体は特に違和感ないです。が、それが効くかもよくわかっていません。
この時欠陥はユースケース間にのみ存在する
文脈としては、単体ユースケースで検証を行った後に複数のユースケースをつなげて検証を行った場合に、ということです。確かにそうで、状態爆発みたいなものを防げるのかもしれません。
過去研究は、ユースケース記述におけるシステムとアクタの間のやり取りから状態を抽出し、状態遷移モデルとしている。しかし、検証内容に関する情報はユースケース記述内に散在している
過去研究の考え方はとても理解しやすいです、システムとアクタのイベント/アクションによってシステムとアクタの合成された状態が遷移する、という考え方で理解できるからです。ちょっとわからないのは「しかし」以降です。過去研究のやり方で何が漏れるのか、が理解できていません。
検証内容を決める際に、ユースケース記述を分析しなければならない
なんとなく分かった気がします。過去研究では、フローの各ステップでの振る舞い（アクション）は分析されることなく、イベントの連続とそれによる状態の遷移としてのみ書かれていたのだと思われます。よって、期待される振る舞いを明示する必要があったということだと思われます。なるほど。もしそうだとすると、過去研究でのモデル検証はとても限定された範囲のものだということになりますね。うーん。
実験の結果、各ユースケース記述の系列や、複数のユースケース間に潜む欠陥が検出できると判り
いいですね、どんな種類の欠陥か、とかは気になりますが。。試してみたい。
がぜん興味が湧いてきました。