チュートリアル
VDM++による形式仕様記述
2011/01/25
■チュートリアルの趣旨と概要
本チュートリアルでは，形式手法VDM++によるソフトウェアの仕様記述と検証・分析について，ツールを使った実習を交えて解説していただきます．
ソフトウェア開発では，開発の早い段階での誤りが後の工程へと引き継がれることに起因する，システムの信頼性低下や手戻りによるコスト増大が大きな問題となっています．このため，開発の初期段階の仕様書や設計書等の中間成果物に対して，科学的・系統的に分析・検証を行い誤りを除いておくことが重要であると考えられます．
そのためのアプローチとして，数理的な基礎のもとにモデル化と検証・分析を行う，形式手法が最近注目されています．しかし，これまで開発者が身につけてきたものとは異なる知識・スキルが求められるので，敷居が高いという側面があるのも事実です．
本チュートリアルでは，ライトウェイトな形式手法であるVDMをとり上げます． VDMでは，システムの状態を表す変数やそれに対する操作を抽象的にモデル化し，インタプリタ実行によるテストを中心とした方法で検証・分析を行います．このため，一般の開発者にとって身近な方法により，実装詳細を捨象した形での仕様の厳密化・明確化，および実行を通した検証・分析を行うことができます．
本チュートリアルでは，形式手法としてのVDMの考え方・アプローチと，オブジェクト指向に基づいたVDM++言語を使った仕様記述について，解説していただきます．さらに，ツールを用いた仕様の実行と検証・分析方法についても，具体例に基づく実習と実演を交えて，説明していただきます．
講師には，国立情報学研究所の助教であり，先端ソフトウェア技術者育成プログラムで講師もされている，石川冬樹氏をお招きしました．
受講対象は，ソフトウェア仕様の形式記述・検証や開発早期におけるプロトタイピングに関心を持っている技術者の方，これから形式手法分野の研究をはじめようとされる学生の方，ライトウェイトな形式手法の導入に興味のあるプロジェクトリーダーの方などです． 多数の皆様のご参加をお待ち申し上げております．
【プログラム】
- VDM概観
- 形式手法の考え方
- VDMの位置付け・アプローチ
- 例題解説・実習
- 抽象モデル化のためのVDM++構文
- VDM++による仕様記述と実行・テスト・分析
- 発展事項解説・実演
- 異なるモデル化方針に基づく例題の発展
- その他ツール機能の解説・実演（UMLとの連携，Javaコード生成等）
- 適用方針に関する議論
- まとめ
- 活用事例紹介
- 最新動向の紹介
- 参考書ガイド
時間の都合でプログラムは若干変更される場合があります.
【ツール】
- 実習には会場備え付けの機器を使用しますので，参加者が個別にPCを持参される必要はありません．
■講師
石川 冬樹氏 (国立情報学研究所)
■日時
- 2011年1月25日(火)
- 午前10時00分～午後5時（受付開始：午前9時半）
■会場
国立情報学研究所 20階ミーティングルーム(2009, 2010)
- 〒101-8430 東京都千代田区一ツ橋２－１－２
- Web: http://www.nii.ac.jp/introduce/access1-j.shtml
- 最寄り駅: 東京メトロ半蔵門線／都営地下鉄三田線・新宿線「神保町」A8出口，もしくは， 東京メトロ東西線「竹橋」1b出口から徒歩3～5分
■募集定員
32名(先着順)
■参加費
| 一般会員 | 10,000円 |
| 一般非会員 | 15,000円 |
| 学生会員 | 3,000円 |
| 学生非会員 | 6,000円 |
- 会員割引の対象となるのは，日本ソフトウェア科学会ないしNPO法人 トップエスイー教育センターの会員です．
- 日本ソフトウェア科学会への入会は，当日申し込みいただけます．
■申込み方法
- 参加申し込みページからお申し込み下さい．
- 参加費は当日，会場受付でお支払い下さい．引き換えに領収書をお渡しします．
- 定員に達し次第, 本ページに掲載するとともに，申し込みを締め切らせていただきます．
■お問い合わせ先
トップエスイー チュートリアル事務局: E-mail: vdm-tutorial @ topse.jp
トップエスイーは，情報・システム研究機構の登録商標です．
