|
21年度は前年度までの検討成果をベースに、検証モデリング上の問題をより深く検討しながらモデリングメカニズムをリファインすることを目的とし、1)企業での試行例を含む実用規模の検証事例を調査することにより、実用的な形式検証のために必要とされるモデリングへの要求事項の整理、2)それに対応するための具体的なモデリングメカニズムのリファインと、モデリング環境の試作と評価、3)実際のソフトウェア開発のコンテキストの中で、設計モデリングと検証モデリングとを体系化するためのソフトウェア工学的な観点からの検討と考察を行った。
上記の結果、以下の成果が得られた。1)実際の検証においては複数の検証性質に関する検証を行うことが多いが、類似した検証性質に対しては必要な検証モデルも類似性を持っている。そうした類似した検証モデルは相互に横断的な差異を持つ状況が複数あることが分かった。2)上記を踏まえ、UMLに対して通常のジョインポイントモデルに基づくアスペクト指向拡張を施した検証モデリング環境を試作した。基本となる検証モデルを支配的な構造として構築しておき、個々の検証性質に応じたモデル上の差異をアスペクトとして定義し検証の際にウィーブすることで、横断的な差異を効果的に扱うことができ、1)での状況での検証への有効性が確認された。3)一方、検証モデリングはどのような性質を検証するかという目的にそった適切な抽象である必要があるが、適用事例をみると必ずしもそういう観点からのモデリングがなされておらず妥当な検証となっていない場合もあった。有効な検証のためには、検証性質を明示化し、その検証に必要十分なモデルを構築するための体系だった手順が必要であると考える。次年度はモデリングメカニズムだけでなく、検証手法に踏み込んだ検討を進める予定である。
|
