トップエスイー修了制作 VDMにおける状態遷移ベース仕様記述と検証の提案（株）CSKシステムズ植木雅幸開発における問題点手法・ツールの適用による解決「形式手法は難しい」。形式手法に対してしばしば聞かれる意見である。それは、形式手法の中では容易な部類のVDMにも例外ではない。そこには、「VDM」という手法を便利に使う方法や使いやすくするためのノウハウが少ないという問題がある。本提案は、難しいと言われるVDMの利用を、より効果的に、より使いやすくすることを目指す。そのために、利用者の多いUMLの状態遷移図から、VDM仕様を生成する方法論を提案している。また、VDM記述のベースを状態遷移とし、それを表現するためのVDM状態遷移フレームワークを作成した。本提案のオーバービュー UML 状態遷移図 VDM 修了制作の範囲 VDM状態遷移フレームワーク生成方法論 VDM仕様今後、本提案の仕組みをツールによって自動化することを検討テストシナリオ状態遷移図とVDMの連携 VDM状態遷移フレームワーク状態遷移図停止 doStateTransition mapping 再生ボタン押下 [ DVDあり and トレイ閉 ] / 再生する再生 mapping receiveEvent doAction VDMテストシナリオ記述 Test Case シナリオイベント列 ex) 電源ボタンを押すトレイ開閉ボタンを押す再生ボタンを押す setState 継承 VDM仕様記述トップエスイー ∼サイエンスによる知的のものづくり教育プログラム∼ 国立情報学研究所トップエスイー：サイエンスによる知的ものづくり教育プログラム National Institute of Informatics 文部科学省振興調整費産学融合先端ソフトウェア技術者養成拠点の形成文部科学省科学技術振興調整費産学融合先端ソフトウェア技術者養成拠点の形成