カテゴリー: 教育事業

■講師
・羽深 修（NTTデータ先端技術株式会社）
・中井 悦司（レッドハット株式会社 ）

■プログラム：
第一部（担当講師：羽深）
・Eucalyptusとedubase Cloud（講義）
・edubase CloudによるIaaSインフラ活用演習（ハンズオン）

第二部（担当講師：中井）
・IaaSクラウドを支えるサーバ・インフラ技術（講義）
・edubase Cloudによるサーバ・インフラ技術活用演習（ハンズオン）

※演習は会場備え付けのPCを使います。

■プログラム：
10:00-12:00 PAT Model Checking System
講演者：Jin-Song Dong 准教授, The National University of Singapore
13:30-16:30 PATハンズオン～ふれながら学ぶモデル検査
講師: 藤本 洋 氏(キャッツ(株))

※注意：午前の第１部は英語での講演となります（通訳なし）
※ 午後の部は会場に用意されたシンクライアントを使って演習を行います。ご自身のPCをお使いになりたい方は、以下のWebサイトからツールをインストールしてご持参くさい。
http:/pat.comp.nus.edu.sg/

■プログラム詳細
=== 第一部: PATチュートリアル ===
時間: 10:00-12:00
Title: PAT Model Checking System
講演者：Jin-Song Dong博士(the National University of Singapore・准教授)

[概要]
Popular model checkers like SPIN, SMV and FDR are designed for specialized domains and are based on restrictive modeling languages.
In this tutorial, we introduce our latest effort on combining the　expressiveness of state, event, real-time and probability based languages with the power of model checking. We present a process analysis toolkit (PAT , http://pat.comp.nus.edu.sg), which is a self-contained verification system for system specification, simulation and verification. PAT supports a wide range of modeling languages including CSP# (short for communicating sequential programs). The idea is to treat sequential terminating programs, which may indeed be C# programs, as internal events. The result is a highly expressive modeling language which covers many application domains.
Since PAT is released 3 years ago, it has attracted 1300+ registered users from 300 organisations world wide.

[講演者プロフィール]
Jin-Song Dong received Bachelor (1st hon) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995-1998, he was a Research Scientist at the Commonwealth Scientific and Industrial Research Organisation in Australia. Since 1998 he has been in the School of Computing at the National University of Singapore (NUS) where he is currently Associate Professor and a member of PhD supervisors at NUS Graduate School. He is on the editorial board of Formal Aspects of Computing Journal and Innovations in Systems and Software Engineering, A NASA Journal. His research interests include
formal methods and software engineering. Some of his research work can be found at: http://www.comp.nus.edu.sg/~dongjs

=== 第２部: PATハンズオン～ふれながら学ぶモデル検査～
時間：13:30-16:30
講師: 藤本 洋 氏(キャッツ(株))

[概要]
本セミナーでは、プロセス代数(CSP)に基づくモデル検査ツールPAT (Process Analysis Toolkit)の基本的な使い方を理解します。実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法を 解説します。

[講師プロフィール]
電気通信大学電気通信学研究科博士前期課程(情報工学）修了今までかかわった分野は銀行系(第三次オンライン）、ICカードシステム、電子手帳組み込みの ソフト、物理現象のシミュレーションと可視化、医療系システム、車載ネットワーク、モデル変換など。現職ではツール開発と形式手法ツールを担当する。現在、キャッツ株式会社　プロダクト事業本部 技術企画第２グループ　技術マネージャ。

本セミナーは二部に分かれており、どちらか一方だけご参加いただくこともできます。講演，チュートリアルは日本語で行われます。
参加ご希望の方は，下記よりご登録をお願いいたします:
http://grace-center.jp/regist/seminar
準備の都合上，第2部(チュートリアル)に参加される方は必ず前日までにご登録ください。
第二部は、NPO法人 トップエスイー教育センター主催ですので、同センター会員の方は優先してご参加頂けます。
なお、定員になり次第締め切らせていただきますので、ご了承ください。
※講演内容、場所等が変更になる場合があります。

ブレッドボード（差し込み式の配線板）を使いますので、ハンダ付けの必要はありません。ハードウエアの作成は初めてという方も参加できます。ワークショップでは、国産のフィジカルコンピューティング用のデバイス(Pepper(‡))を利用します。必要な機器は、すべて参加費に含まれております。USBに接続可能なノートパソコンのみご持参下さい。

【セミナーに含まれる機材】
・電流センサ組み立て部品　一式
・Pepper フィジカルコンピューティング用のデバイス
【持ち込みをお願いする機材】
・Windows / MacOSXの動くパソコン。
・USBポートがあること。
【参考図書】
・桑田 喜隆，Gainer互換Pepperでフィジカル・コンピューティング，CQ出版
【関連図書】
・「FunnelとPepperを使って省エネ・センサを作ろう」、エレキジャックNo.14 特設記事(1)、フィジカル・コンピューティング・デバイスの活用事例、 CQ出版

(†)フィジカルコンピューティングについては、情報処理8月号(Vol.52,No.8)の特集「夏休み工作のためのフィジカルコンピューティング」をご覧ください。

(‡) Pepperは、下の写真のようなキットになり、受講料に含まれます。（測定器は受講料に含まれません）

8/8（月）1日目：形式手法概論
・ 形式手法の位置づけ・基本的な考え方
・ VDM，SPINの位置づけ・基本的な考え方

8/9（火） 2日目：VDM++入門
・ VDM++言語，Overture IDE/VDMToolsを用いた形式仕様記述入門，演習

8/10（水）3日目：SPIN入門
・ SPINを用いたモデル検査入門，演習

8/11（木） 4日目：形式手法ツール概論
・ VDM，SPINと対比しての様々な手法・ツールの紹介

8/12（金） 5日目：応用事例紹介
・ 応用事例の調査報告や適用ガイダンス等の紹介