第59回 SEA関西プロセス分科会のご案内
形式的仕様記述手法 VDM ワークショップ
講師
酒匂寛（Designer’s Den）
栗田太郎（フェリカネットワークス）
小田朋宏（SRA）
佐原伸（法政大学大学院情報科学研究科兼任講師）
主催 ：ソフトウェア技術者協会 関西支部 プロセス分科会
後援 ：独立行政法人 情報処理推進機構
日時 ：2014年8月30日(土) 10:00～18:00 (9:45 開場)
会場 ： 株式会社SRA 関西事業部 会議室
〒541-0058 大阪市中央区南久宝寺町3-1-8
本町クロスビル2F
内容 ：
ITシステムが社会の様々な分野に浸透し，その重要性を増すに従って，様々な立場・背景の関係者がその仕様を誤解なく理解し，開発を矛盾無く進めていくことのできる方法論・手法が求められています．その為に，数理的な理論に基づく厳密な定義と分析・検証を可能とする「形式手法」が注目されています．
「形式手法」は，長いコンピュータサイエンス・ソフトウェア工学の歴史の中で研究が積み重ねられ，近年，理論・実装面の進展やハードウェア性能の向上に伴って，現実のシステムへの応用が進みつつあります．
今回のワークショップでは，形式手法の中でも特に長い歴史と実績を持つ手法・環境であるVDM（Vienna Development Method）を取り上げ，講演と演習を通して，実践的に理解することを目指します．
講師として，VDMを中心とする形式手法の日本での普及活動に早くから尽力され，技術解説書の翻訳出版やコンサルティング活動で著名な酒匂寛氏・佐原伸氏，フェリカのプロジェクトでVDMの導入で大きな実績を上げた栗田太郎氏，ツール開発で先進的な仕事をされている小田朋宏氏をお招きし，仕様記述の基本概念の解説から実プロジェクトへの導入事例紹介，VDM言語のチュートリアルと演習までを含む，本格的なワークショップとなります．
プログラム ：
10:00 – 11:00 講演「厳密な仕様の位置付けと意味」（講師 酒匂寛）
11:00 – 12:00 講演「システム開発への形式手法の適用による品質の確保」
（講師 栗田太郎）
12:00 – 13:00 昼休み
13:00 – 15:00 VDM言語チュートリアル（講師 小田朋宏）
15:00 – 17:00 VDMPadによる仕様記述演習（講師 佐原伸）
17:00 – 18:00 全員で質問大会
講演「厳密な仕様の位置付けと意味」
厳密な仕様の位置づけと意味について，集合・列・写像の概念を援用しながら，以下
の観点から考察します．
課題ー仕様ー設計
言葉の曖昧さと形式仕様記述
問題領域と機械（指示と定義）
事前・事後・不変条件
講演「システム開発への形式手法の適用による品質の確保」
少人数ではないチームにおいて，設計や実装，テストを正確に行い，品質を確保する
ために，また，運用や保守，派生開発において品質を維持し続けていくために，仕様
や文書はどのような役割を果たすのか．
「おサイフケータイ」の開発プロジェクトにおける，形式仕様記述手法の適用により
品質を確保した事例とともに，文書の記述力やチームのコミュニケーション力を向上
させるための取組みとその結果を紹介しながら，そのことについて考えます．
VDM言語チュートリアル
簡易ウェブIDEであるVDMPadを使って，VDM-SLの主要な構文要素を解説します．
VDM-SLはシステムの状態や機能をモジュール化して記述することができる仕様記述
言語であり，VDMのエッセンスを学ぶことができます．
VDMPadによる仕様記述演習
大規模システムの仕様記述に用いられた手法のエッセンスを，小さな演習を通して伝
授します．
演習の環境について ：
演習を行う為，参加の際にはパソコンの持参をお願いいたします．
演習では，講師の小田朋宏氏により開発されたツール “VDMPad” を使用します．
講師のパソコンをVDMPadのサーバにして，Webブラウザでアクセスして使用しますの
で，パソコンには事前に google chrome または firefox のインストールをお願いします．
パソコンには Wifi 接続の機能が必要となります．
なお、Mac または Linux をお使いの方は、VDMPadは以下よりダウンロードできます．
（Windowsは未対応）
http://sourceforge.net/projects/vdmpad/
また，VDMに関する技術情報が以下のWebページで公開されていますので，ご参照くだ
さい．
http://www.vdmtools.jp/
※ PCをご持参できない場合，演習は他の参加者とのペア作業，または見学となりますの
で，ご了承下さい．
※ 会場には外部とのインターネット接続の設備はありません．
講師紹介
酒匂寛（さこう ひろし）
有限会社デザイナーズデン代表取締役社長
開発環境，構造化手法，オブジェクト指向，開発方法論などに80年代より取り組む．
大規模ミッション・クリティカルシステム，リアルタイムシステム，統合開発環境な
どの調査，開発，コンサルティングに携わる．
主な訳書
（バートランド・メイヤー）「オブジェクト指向入門」
（ジョン・フィッツジェラルド他）「VDM++によるオブジェクト指向システムの
高品質設計と検証」
（マイケル・ジャクソン）「ソフトウェア要求と仕様」．
栗田太郎（くりた たろう）
1971 年生まれ．1999 年からソニー，2004 年からフェリカネットワークスにてモバ
イル FeliCa の開発に携わる．形式手法を活用したソフトウェア開発やプロジェクト
マネジメント等に従事．
博士（情報科学）．
小田朋宏（おだともひろ）
1969年生まれ．1994年より株式会社SRA．同社米国ボウルダー研究所勤務を経て2010
年より同社先端技術研究所研究員．VDMPadの開発をはじめ，形式手法の適用範囲を
広げるための研究開発に携わりながら，Smalltalk，Python，Haskellによるソフトウェ
ア受託開発およびオープンソース開発に従事．
2003年度未踏プロジェクト．
佐原伸（さはら しん）
1951年生まれ．1975年から野村コンピュータシステム（現野村総合研究所），
SRA，SCSKなどを経て，2011年から法政大学大学院情報科学研究科兼任講師．
UNIX導入による開発環境構築，構造化手法導入による証券オンラインシステム開発，
オブジェクト指向導入による原発のシミュレーションツール開発，形式手法導入によ
る証券バックオフィスシステムとおさいふケータイの開発などに関わる．
Formal Method Europe会員，VDM Langauge Boardメンバー．
参加費用：
SEA正会員：1,000円
SEA賛助会員：1,000円
学生：500円
一般：2,000円
※ 懇親会参加費は別途実費負担
定員 ：16名
申込方法：
以下のペ‐ジからお申し込みの受付を行っております．
http://kokucheese.com/event/index/199865/
### 8/29(金)21:00までにお申し込みください ###
ご注意）
• 受付は先着順で，定員になり次第〆切とさせていただきます．
• メール，FAXなどWebページ以外からの申し込みは受け付けておりません．
• お申し込みの受付け後，確認メールが自動的に返送されます．確認メールを印刷し，
当日受付時に持参ください．
• 当日は休日につきビルの玄関が閉まっています．入館にはスタッフの案内が必要で
すので，9:45〜10:00の間に入館していただくようお願い致します．万一，入館が
遅れる場合は，必ず以下のメールアドレスまで，入館予定時刻のご連絡をお願い
致します．
seakansai-req@sea.jp
• 申し込み手続きについて不明点などございましたら下記までご連絡ください．
seakansai-req@sea.jp
• 参加費は当日会場受付にて現金でお支払いください
• 領収書が必要な方は，申し込み時に「領収書要」にチェックしてください．