本文を印刷する

情報処理技術者試験

対象を如何にモデル化するか? (VDM++入門)
〜仕様のモデル化の極意を教えます!!〜[二日コース]

開催情報

  2013年11月にご好評をいただいたワークショップを再び開催します。本ワークショップでは、形式手法で仕様を明確にするモデル化∗1の技術について、実際に課題演習を通して学んでいただきます。仕様記述言語VDM++の基礎とVDM開発支援ツールVDMToolsの基礎を学び、モデル化の課題演習を通じ、VDMを用いたモデル化の手順を学習することで、実際の現場へ形式手法を適用するイメージを掴むことができます。

(∗1)ここでのモデル化とは、システムの仕様に内部矛盾が無いかを検証(正当性検証)し、ユーザーの要求に合っているかを確認する(妥当性確認)モデルを作成することです。

  本ワークショップは、2月4日と2月12日に開催する二日コースです
  ・2日とも無線LAN機能付きのノートパソコンをご持参ください(必須)
  ・1日のみの受講は受け付けておりません。

主催 独立行政法人情報処理推進機構 (IPA)
技術本部 ソフトウェア高信頼化センター
開催日時 第1日目:2014年2月4日(火)】10:00〜17:30
第2日目:2014年2月12日(水)】10:00〜17:30
開催場所 〒113-6591
東京都文京区本駒込2-28-8 文京グリーンコートセンターオフィス13階
独立行政法人情報処理推進機構内 会議室
アクセスマップ
定員 30名
参加費 ■各日:2,000円(税込)
・参加費は、会場受付時に現金でお支払いをお願い致します。
・受付にて、領収証を発行致します。
・お釣りのないようにご用意をお願い致します。
・両日それぞれの申し込みが必要です。
募集対象 1.仕様を書くために必要な離散数学の基礎を勉強したい方
  ・集合論、述語論理(命題論理+3つの論理式)の基礎
2.仕様記述言語VDM++で仕様を書くための初歩を知りたい方
3.形式手法適用に関し専門家の意見を聞きたい方
4.2月4日と2月12日の両日とも受講可能な方(1日のみの受講は受け付けておりません)
本ワークショップは、2月4日と2月12日の二日コースです。

 2日とも無線LAN機能付きのノートパソコンをご持参ください(必須)。
事前準備 ※本ワークショップでは、学習をスムーズに進めるため、参加者の皆様に両日とも事前学習をお願いします。

1日目の事前学習:VDM++言語の学習とツールの基本機能の習得
下記ファイルをダウンロードし、ワークショップ当日ご持参いただくノートパソコンで学習してください。
VDMToolsVDM++入門PDF 
形式記述サンプル[zip形式]

1日目の追加演習
MostSimpleSpec [zip形式]

2日目の事前学習:例題によるモデル化の自主学習
副読本「対象を如何にモデル化するか?」第7章演習問題7.1図書館システムについて下記の内容を実施してください。
  1.ユースケースレベルの要求仕様を作成してください。
  2.陰仕様を作成してください。
  3.陽仕様を作成してください。
  4.回帰テスト(余裕のある方は実施してください)
第8章が解答編になっていますので比較してみてください。
下記形式記述サンプルにも解答がありますので、ご覧ください。

「対象を如何にモデル化するか?」形式記述サンプル付[zip形式]

2日目の追加演習
UniqNumSimpleEx [zip形式]

■使用条件
事前学習資料は、次の使用条件の下でご利用ください。

  1. 本資料の著作権は、独立行政法人 情報処理推進機構が保有しています。
  2. 本資料は著作権法による保護を受けており、本資料の使用者は、本資料の全部または一部を項番3に定める場合を除き、独立行政法人 情報処理推進機構の許諾なく無断で複製、改変、公衆送信、販売、出版、翻訳/翻案等の著作権法上の利用行為は営利目的、非営利目的に関わらず禁じられています。
  3. 独立行政法人 情報処理推進機構は、本資料の使用者が、以下の著作権表示を明記することを条件として、①及び②の行為を行うことを許諾します。
    著作権表示:Copyright©2013 独立行政法人 情報処理推進機構
    ①本資料の全部または一部を複製すること。
    ②本使用条件に記載されている使用条件を配布先に遵守させることを条件に本資料の複製物を無償で再配布すること。
  4. 独立行政法人 情報処理推進機構は、本資料が第三者の著作権、特許権、実用新案権等の知的財産権を侵害しないことを一切保証するものではなく、また、本資料の内容に誤りがあった場合でも一切責任を負いかねます。
  5. 独立行政法人 情報処理推進機構は、本使用条件に記載された許諾内容を除き、独立行政法人 情報処理推進機構または第三者の著作権、特許権、実用新案権等の知的財産権に基づくいかなる権利を許諾するものではありません。
  6. 独立行政法人 情報処理推進機構は、本資料のシステム開発への利用、開発されたシステムの使用、及び当該システムの使用不能等により生じるいかなる損害についても、なんら責任を負うものではありません。
  7. 本資料を海外へ持ち出す場合及び非居住者に提供する場合には、「外国為替及び外国貿易法」の規制及び米国輸出管理規則等外国の輸出関連法規を確認のうえ、必要な手続きを行って下さい。
  8. 【形式記述サンプル】には、オープンソースのVDMUnitが含まれております。
    VDMUnitの著作権と使用条件は下記となります。
    VDMUnit - an open-source framework for formal specification of test suites in VDM++. Copyright (C) 2005 Marcel Verhoef
    This program is free software: you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation, either version 3 of the License, or (at your option) any later version.
    This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details. You should have received a copy of the GNU General Public License along with this program. If not, see http://www.gnu.org/licenses/.
  9. 本資料へのお問い合わせについては、独立行政法人 情報処理推進機構 技術本部 ソフトウェア高信頼化センターまでご連絡下さい。
配布物 ・「対象を如何にモデル化するか?」製本版

※参加できない場合は、必ずキャンセル処理を行ってください。
※お席に限りがありますので、一部署より多くの方がご参加の場合には調整をお願いさせていただく場合があります。

プログラム

■2月4日(火):対象を如何にモデル化するか? (VDM++入門) その1

時刻 概要
9:30 受付
10:00〜
17:30
1 VDMToolsの説明
2 VDM++言語入門
3 対象を如何にモデル化するか?
4 Q&A


自主学習としてお願いしている、事前課題の結果を振り返りながら、VDMToolsの説明およびVDM++言語の入門レベルを学びます。その上で、仕様記述とは何か、仕様のテストとは何か理解し、モデル化の一般手順を学んでいただきます。

IPA/SEC 連携委員
法政大学
大学院情報科学研究科
佐原  伸 氏

IPA/SEC 連携委員
九州大学 主幹教授
アーキテクチャ指向フォーマルメソッド研究センター長
伊都図書館長
大学院システム情報科学研究院 副研究院長
荒木  啓二郎 氏

IPA/SEC 連携委員
有限会社 デザイナーズ・デン
代表取締役社長
酒匂  寛 氏

株式会社メタテクノ
応用技術開発部
プロジェクトマネージャー
宮本  陽子 氏

IPA/SEC 連携委員
新谷ITコンサルティング 代表
新谷  勝利 氏

■2月12日(水):対象を如何にモデル化するか? (VDM++入門) その2

時刻 概要
9:30 受付
10:00〜
17:30
1 図書館問題解答例説明
2 受講者の解答例について討議
3 Q&A


図書館問題解答例を説明し、対象を如何にモデル化するかについて具体的なイメージを掴んでいただき、受講者の解答例についての討議を通し、より理解を深めていただきます。

IPA/SEC 連携委員
法政大学
大学院情報科学研究科
佐原  伸 氏

IPA/SEC 連携委員
九州大学 主幹教授
アーキテクチャ指向フォーマルメソッド研究センター長
伊都図書館長
大学院システム情報科学研究院 副研究院長
荒木  啓二郎 氏

IPA/SEC 連携委員
有限会社 デザイナーズ・デン
代表取締役社長
酒匂  寛 氏

株式会社メタテクノ
応用技術開発部
プロジェクトマネージャー
宮本  陽子 氏

IPA/SEC 連携委員
新谷ITコンサルティング 代表
新谷  勝利 氏

 

参加申込み

※両日それぞれの申し込みが必要です。
【第1日目】2月4日(火)お申し込みはこちら
【第2日目】2月12日(水)お申し込みはこちら