プロセス分析ツールPATによるモデリングとモデル検査(3/17)

セミナー概要

日時:
2016年3月17日(木)
13:30-17:00(受付開始: 13:00)
会場:
国立情報学研究所 国立情報学研究所 20階 ミーティングルーム(2009/2010)
概要:
並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼びしてリアルタイム性のモデル検査のチュートリアル、および、ハンズオンセミナーを開催いたします。第1部は、ツールの 提案者から直接最新のモデル検査ツールが学べるまたとない機会となっています。また第2部では、実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法、時間制約表現の機能など学べます。ぜひこの機会にお誘いあわせの上、ご参加ください。

■プログラム:
13:30-15:00 第1部:Event-Strategy Analytics: The PAT approach
講演者:Jin-Song Dong 准教授, The National University of Singapore

15:10-17:00 第2部:PATハンズオン〜PATによるモデリングとモデル検査の実際〜
講師: 藤本 洋 氏(イーソル株式会社技術本部)

※注意:第1部は英語での講演となります(通訳なし)。
※第2部の演習のため、以下のWebサイトからPATツールをご自身のPCにインストールしてご持参くさい。備え付けのPCのご利用を希望の方は申込時に申請してください。会場にはキャリアのホットスポットが使えますが、ゲスト用無線LANアカウントはございません。
http://pat.comp.nus.edu.sg/

■プログラム詳細
=== 第一部 ===
時間: 13:30-15:00
Title: Event-Strategy Analytics: The PAT approach
講演者:Jin-Song Dong博士(the National University of Singapore・准教授)

[概要]
Abstract: Popular model checkers like SPIN, SMV, and FDR are designed for specialized domains and are based on restrictive modeling languages. In this talk, we introduce our latest work on combining the expressiveness of state, event, real-time, and probability-based languages with the power of model checking. We present the process analysis toolkit (PAT), which is a self-contained reasoning system for system specification, simulation, and verification. PAT currently supports a wide range of 20 different modeling formalism/languages, including CSP# (short for “communicating sequential programs,” which is based on Hoare’s CSP). 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. Recently, we have successfully applied PAT to AI planning problems [FMSD’13], Sports Analytics [ICECCS’15] and real-time and probabilistic systems [CAV’12’13].These recent research results set a solid foundation for a new research direction; that is to apply model checking as Service to event planning/prediction, strategy analysis and decision making, which we call “Event Analytics”. “Data” are static information where “Event” are more dynamic and often involve causality, communication, timing and probability. Event Analytics can offer a new set of technologies that is beyond static “Data Analytics”. In this seminar, we will introduce PAT system and its vision. (http://www.comp.nus.edu.sg/~pat/)

[講演者プロフィール]
Jin Song Dong received Bachelor (1st class hon) and PhD degrees in Computing from University of Queensland in 1992 and 1996. From 1995 to 1998, he was research scientist at CSIRO 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. He is the deputy director of Singapore-French joint Research lab IPAL. Jin Song is on the editorial board of ACM Transaction on Software Engineering and Methodology and Formal Aspects of Computing. He has been general/program chair for a number of international conferences, including the general chair of 19th FM 2014 in Singapore. Jin Song has been a Visiting Fellow (2006) at Oxford University, UK, and a Visiting Associate Professor (since 2009) at National Institute of Informatics, Japan. He has supervised 24 PhD students to their successful
completion. Many of his PhD students have become faculty members in leading universities around the world. Jin Song and his two former PhD students Jun & Yang have founded the model checker PAT (Process Analysis Toolkit) which has attracted 3000+ registered users from 900+ organizations in 89 countries. Outside of Work, he plays competitive tennis and is a registered tennis coach teaching top ranked junior players in Singapore (including his own 3 kids). He also developed Markov Decision Process (MDP) models for tennis strategy analysis in PAT. (https://www.comp.nus.edu.sg/~dongjs/)

=== 第2部: PATハンズオン 〜PATによるモデリングとモデル検査の実際~
時間:15:10-17:00
講師: 藤本 洋 氏(イーソル株式会社 技術本部)

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

[講師プロフィール]
電気通信大学電気通信学研究科博士前期課程(情報工学)修了。専門は数理モデリング、ソフトウェア開発。経験分野は銀行系(第三次オンライン)、ICカードシステム、物理現象のシミュレーションと可視化、医療系システム、セマンティックWebシステム、車載ネットワーク、形式手法ツールの導入支援、マルチ・メニーコア上で動作するの並列処理ソフトウェア開発支援環境研究開発。現在、イーソル株式会社技術本部所属。エキスパート職。日本PATユーザ会。

定員:
20名(先着順)
※定員に達し次第,申し込みを締め切らせていただきます。
参加費:
一般 3,000円/学生 無料
会員: 無料
※日本ソフトウェア科学会 会員の方も無料となります。
※NPO法人 トップエスイー教育センター会員及び日本ソフトウェア科学会会員の方は、優先的に受講いただけます。
参加申込方法:
参加申込みサイトより必要事項を入力の上、お申込みください。※こちらでPCを準備できますのでご希望の場合は申請時に選択してください。
http://ws.formzu.net/fgen/S53074529/
主催:
NPO法人 トップエスイー教育センター
協力:
国立情報学研究所 GRACEセンター
協賛:
日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ窓口:
セミナーに関するご質問などは、下記アドレスにて承ります。
inquiry_[at]_topse.or.jp ※_[at]_部分を@に変えてください

プロセス分析ツールPATで学ぶ並行プロセスのモデル検査(4/17)[終了]

■日 程:2014年4月17日(木)
■会 場:国立情報学研究所 20階ミーティングルーム1・2(2009, 2010)
■講 師:Jin-Song Dong 准教授(The National University of Singapore),
藤本 洋 氏(キャッツ(株))
■参加費:午前の部:無料、午後の部:非会員は有料

セミナー概要
日 時 2014年4月17日(木) 10:00 ~ 16:30 (受付開始: 9:30)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼びしてリアルタイム性のモデル検査のチュートリアル、および、ハンズオンセミナーを開催いたします。午前は、ツールの 提案者から直接最新のモデル検査ツールが学べるまたとない機会となっています。また午後の部では、実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法、時間制約表現の機能など学べます。ぜひこの機会にお誘いあわせの上、ご参加ください。■プログラム:
10:00-12:00 Event Analytics and Verification: The PAT approach
講演者:Jin-Song Dong 准教授, The National University of Singapore
13:30-16:30 PATハンズオン~ふれながら学ぶモデル検査
講師: 藤本 洋 氏(キャッツ(株))

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

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

今回は、並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス
分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼び
してリアルタイム性のモデル検査技術の導入から最新動向までを講演して頂き
ます。直接最新のモデル検査ツールが学べるまたとない機会となっています。
また、午後は、NPO法人トップエスイー教育センターが主催のハンズオンセミナー
もございます。ぜひ、そちらもご参加ください。

[概要]
Abstract: Popular model checkers like SPIN, SMV, and FDR are designed
for specialized domains and are based on restrictive modeling
languages. In this talk, we introduce our latest work on combining the
expressiveness of state, event, real-time, and probability-based
languages with the power of model checking. We present the process
analysis toolkit (PAT), which is a self-contained reasoning system for
system specification, simulation, and verification. PAT currently
supports a wide range of 20 different modeling formalism/languages,
including CSP# (short for “communicating sequential programs,” which
is based on Hoare’s CSP). 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. Recently, we have successfully applied PAT to AI
planning problems [FMSD’13] and developed verification modules for
real-time and probabilistic systems [CAV’12’13].These recent research
results set a solid foundation for a new research direction; that is
to apply model checking as Service to event planning/prediction,
strategy analysis and decision making, which we call “Event
Analytics”. “Data” are static information where “Event” are more
dynamic and often involve causality, communication, timing and
probability. Event Analytics can offer a new set of technologies that
is beyond static “Data Analytics”. In this seminar, we will introduce
PAT system and its vision. (http://www.comp.nus.edu.sg/~pat/)

[講演者プロフィール]
Bio: Jin Song Dong received Bachelor (1st hon) and PhD degrees in
Computing from University of Queensland in 1992 and 1996. From 1995
to1998, he was research scientist at CSIRO 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. He is the
deputy director of Singapore-French joint Research lab IPAL. Jin Song
is on the editorial board of ACM Transaction on Software Engineering
and Methodology and Formal Aspects of Computing. He has been
general/program chair for a number of international conferences,
including the general chair of 19th FM 2014 in Singapore. Jin Song has
been a Visiting Fellow (2006) at Oxford University, UK, and a Visiting
Associate Professor (since 2009) at National Institute of Informatics,
Japan. He has supervised 16 PhD students to their successful
completion in the areas of formal methods, model checking, theorem
proving, real-time and probabilistic reasoning, web ontology and
pervasive computing. Many of his PhD students have become faculty
members in leading universities around the world. Jin Song and his two
former PhD students Jun & Yang have founded the model checker PAT
(Process Analysis Toolkit) which has attracted 3000+ registered users
from 800+ organizations in 71 countries. Outside of Work, he plays
competitive tennis and is a registered tennis coach teaching top
ranked junior players in Singapore (including his own 3 kids). He also
developed Markov Decision Process (MDP) models for tennis strategy
analysis in PAT with a special case study on Federer vs Nadal.
(https://www.comp.nus.edu.sg/~dongjs/
)
=== 第2部: PATハンズオン~ふれながら学ぶモデル検査~
時間:13:30-16:30
講師: 藤本 洋 氏(キャッツ(株))

[概要]
本セミナーでは、プロセス代数(CSP)に基づくモデル検査ツールPAT (Process Analysis Toolkit)の基本的な使い方を理解します。実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法を解説します。また、今回の演習では、基本的な表現であるCSPモデルに加えて、 CSPに時間制約表現を記述できる様に拡張したTimedCSPのモデルも紹介する予定です。
[講師プロフィール]
電気通信大学電気通信学研究科博士前期課程(情報工学)修了今までかかわった分野は銀行系(第三次オンライン)、ICカードシステム、電子手帳組み込みの ソフト、物理現象のシミュレーションと可視化、医療系システム、車載ネットワーク、モデル変換など。現職ではツール開発と形式手法ツールを担当する。現在、キャッツ株式会社 プロダクト事業本部所属技術マネージャ。

定 員 第一部:36名,第二部:20名(先着順)
参加費 午前はGRACEセミナーとして開催し、参加費無料となります。
午後:非会員:(一般) 5000円、(学生) 無料
※NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会会員、トップエスイー受講生、もしくはキャッツ(株)からの招待状をお持ちの方は、無料で参加いただけます。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
協 賛 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
キャッツ株式会社
参加お申込み 以下の参加申し込みフォームよりご登録をお願いします。
 URL:http://form1.fc2.com/form/?id=906892

【TopSE特別講義】「モデル検査事例演習」(1/6, 13, 26, 2/10開催)[終了]

■日 程:2012年1月6日(金),13(金),26(木), 2月10日(金)
■講 師:早水公二 (株式会社フォーマルテック)
■会 場:国立情報学研究所 20階 ミーティングルーム1・2(2009・2010)

セミナー概要
日 時 2012/1/6 (金) 10:20-17:50 (4コマ)
2012/1/13(金) 10:20-17:50 (4コマ)
2012/1/26(木) 10:20-17:50 (4コマ)
2012/2/10(金) 10:20-16:05 (3コマ)
(受付開始: 10:00)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
〒101-8430 東京都千代田区一ツ橋2-1-2
概 要 本講座は,企業におけるモデル検査推進者の育成を目的としています.モデル検査の実務を想定し,その開始から終了までの全プロセスを意識した演習を行います.通常の検証作業で体験する,検証対象ソフトウェアの開発者からのヒアリング,ソフトウェアのモデル化,モデル検査,結果報告,最終報告書の執筆に至るまで,各フェーズでのポイントを押さえた演習に取り組んでいただきます.演習課題は実システムを基に作成されたもので,ソースコード (C言語) と仕様書の課題のいずれか1つを選択することができます.モデル検査ツールは SMV を使用します.

【スケジュール】
2012/1/6 (金) 10:20-17:50 (4コマ)
2012/1/13(金) 10:20-17:50 (4コマ)
2012/1/26(木) 10:20-17:50 (4コマ)
2012/2/10(金) 10:20-16:05 (3コマ)

※注意: 原則として全日程の参加をお願いいたします.やむを得ない事情で一部の日程に参加できない見込みの方は,あらかじめ事務局までご相談ください.
※本講義は、2012年度にトップエスイーにて開講予定の「モデル検査事例演習」をベースにした「特別講義」です。正式開講に先立ち,トップエスイーの受講生とNPO会員の皆様に特別に開講いたします。

【前提知識】
SMV に関する基本的な知識が必要です.講義中に簡単な復習は行いますが,SMV に触れたことが無い場合には,事前に操作方法,モデルの作成方法,CTL 式の作成方法を学習しておくことを強く推奨します.「設計モデル検証(応用編)」もしくは 2011 年のトップエスイー教育センター主催セミナー「SMVで学ぶモデル検査入門」を受講済みであれば問題ありません.なお,後者は近日中に edubase Stream (http://stream.edubase.jp/) で公開します.

内容のレベル 応用
講 師 早水 公二 (株式会社フォーマルテック)
対 象 一般 ※10名(先着順)
参加費 会員 無料
一般非会員 50,000円(税込み)
学生非会員 16,000円(税込み)
※NPO法人 トップエスイー教育センター会員は優先的にご参加いただけます。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
お問合せ セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

 

プロセス分析ツールPATで学ぶ並行プロセスのモデル検査(10/24開催)[終了]

■日 程:2011年10月24日(月)
■会 場:国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師:Jin-Song Dong 准教授(The National University of Singapore), 藤本 洋 氏(キャッツ(株))
■参加費:無料
※セミナータイトルが講演内容に合わせて若干変更になりました。ご了承ください。(2011/10/13)

セミナー概要
日 時 2011年10月24日(月) 10:00~16:30(受付開始: 9:30)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼びしてリアルタイム性のモデル検査のチュートリアル、および、ハンズオンセミナーを開催いたします。ツールの提案者から直接最新のモデル検査ツールが学べるまたとない機会となっています。また午後の部では、実際にツールを使っていただきながら、具体的な使い方を解説いたします。
ぜひこの機会にお誘いあわせの上、ご参加ください。

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

※注意:午前の第1部は英語での講演となります(通訳なし)
※ 午後の部は会場に用意されたシンクライアントを使って演習を行います。ご自身の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

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

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

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

内容のレベル 入門
対 象 一般 
※ 定員 第一部:30名,第二部:20名(先着順)
参加費 無料
※NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会に所属されている方は優先的にご参加いただけます。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
協 賛 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ先 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp
講演資料 午前の部:資料1資料2

VDM、SPINから始める形式手法入門(8/8-12開催)[終了]

■日 程:2011年8月8日(月)-12日(金) 各日とも17:30-19:30(17:00受付開始)
※初日のみ参加も可能です。
■会 場:国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師:国立情報学研究所 石川 冬樹,田辺 良則
■参加費:一般会員 無料、一般非会員 18,000円(税込み)
学生会員 無料、学生非会員 10,000円(税込み)
※初日のみ参加の場合、参加費は無料です。
※一般・学生非会員の参加費の記載が誤っておりました。お詫びいたします。(8月2日訂正)

セミナー概要
日 時 2011年8月8日(月)-12日(金) 各回 17:30-19:30(17:00受付開始)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 近年,ソフトウェア開発における効率的な信頼性向上のためのアプローチとして,形式手法が注目され話題になっています.一方で,言葉は聞いたことがあってもなかなか実際に自身で触れる機会がなく,ニーズに合うものなのかよくわからないという方も多いのではないかと思います.また「形式手法」とはあくまでアプローチの総称であり,実際の活用においては多様な手法・ツールから問題に適したものを選んだり,その活用方針を議論し定めていったりする必要があります.本セミナーでは,まず形式手法の考え方を知るため,また実感するため,代表的な手法・ツールとしてVDM,SPINの概要を紹介するとともに,それらを使った簡単な演習を行います.加えて,それらとの比較を通して他の手法・ツールの概要についても紹介するとともに,近年盛んに公開されている応用事例の調査報告や適用ガイダンス等についても紹介します.各回の構成は下記の通りです.

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日目:応用事例紹介
・ 応用事例の調査報告や適用ガイダンス等の紹介

内容のレベル 入門
講 師 石川 冬樹,田辺 良則
対 象 一般 ※ 定員 36 名(先着順)
参加費 一般会員 無料、一般非会員 18,000円(税込み)
学生会員 無料、学生非会員 10,000円(税込み)
※初日のみ参加の場合、会員種別に関わらず参加費は無料です。
※NPO法人 トップエスイー教育センター会員は会員としてお申込ください。
※参加費の一部(10%)を、東日本大震災の義援金として寄付いたします。
※「会員」:NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会に所属されている方は会員割引の対象となります。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

【TopSEチュートリアル】MindStormで学ぶ、UPPAALによる時間制約の検証(6/6開催)[終了]

■日 程:2011年6月6日(月)
■会 場:国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師:(株)東芝 長谷川 哲夫、イーソル(株) 宇佐美 雅紀

セミナー概要
日 時 2011年6月6日(月) 10:00-17:00(9:30受付開始)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 ソフトウェア開発の上流工程で信頼性を向上させる技術として,形式手法の一つであるモデル検査による設計検証が注目されています。モデル検査は、システ ムが取り得る全状態を網羅的に検査し、システムが要求された性質や挙動を満たさない状態に到達する場合は、その状態に至るまでのパスを発見することができ ます。これにより、微妙なタイミングや多くの条件が重なることで発生する不具合の発見・解析に有効です。
本チュートリアルでは,特に時間制約を扱えるモデル検査ツールUPPAALを使って検証する方法について解説します。前半では、時間に関する情報を UPPAALでモデル化し、時間制約を検証する手法の概要を説明します。後半では、LEGO Mindstorm製のブロックソーター(LEGOブロックを色分けする機械)を例題に、実世界の時間制約をモデル化し検証する実習を行います。さらに、実際の開発におけるUMLによる設計モデルと、UPPAALによる検査モデル、ソースコードとの関係を考えていきます。

下記がチュートリアルの内容になります。

・モデル検査ツールUPPAAL概論
・UPPAALの紹介
・UPPAALのモデル
・時間制約の検証
・時間が扱えると何がうれしいか
・モデルに表現すべき時間の種類とモデル化に際しての留意点など
・例題を基に、UPPAALによる検証を実習
・LEGO Mindstorm製ブロックソーターを用いてUPPAALを使った時間制約の検証を実習する

※トップエスイーチュートリアルは、GRACEセンターが実施しているトップエスイーの科目の内容を分りやすく1日で学べるチュートリアルです。本チュートリアルの詳細は、トップエスイーの開講科目「性能モデル検証」で学べます。詳細は事務局までお問い合わせください。

内容のレベル 応用
講 師 (株)東芝 長谷川 哲夫、イーソル(株) 宇佐美 雅紀
対 象 一般 ※ 定員 36 名(先着順)
参加費 一般会員 10,000円(税込み)、一般非会員 23,000円(税込み)
学生会員 3,000円(税込み)、学生非会員 8,000円(税込み)
※NPO法人 トップエスイー教育センター会員、日本ソフトウェア科学会、に所属されている方は会員としてお申込ください。
※キャッツ株式会社からの割引券をお持ちの方は、会員割引の対象となります。
※参加費の一部(10%)を、東日本大震災の義援金として寄付いたします。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
協 賛 日本ソフトウェア科学会 ソフトウェア工学の基礎研究会、キャッツ株式会社
お問合せ先 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

SMVで学ぶモデル検査入門(5/26開催)[終了]

■日 程:2011年5月26日(木)
■会 場:国立情報学研究所 20階ミーティングルーム(2009, 2010)
■講 師:早水 公二(株式会社フォーマルテック)

セミナー概要
日 時 2011年5月26日(木) 10:00-17:00(9:30受付開始)
会 場 国立情報学研究所 20階 ミーティングルーム1・2(2009, 2010)
概 要 近年、産業界で注目を集めている形式手法の1つであるモデル検査の入門講座です。モデル検査はシステムが取り得る全状態を網羅的に検査するため、要求された性質や挙動を満たさない状態が1つでもあれば、その状態に至るまでのパスを発見することができます。微妙なタイミングや多くの条件が重なることで発生する不具合の発見・解析に非常に有効です。本セミナーでは、モデル検査の概要に加えて、企業での取り組みやデモ、多くの例題を交えながら初心者の方にも分かりやすく説明します。また、演習問題も用意していますので、実際にモデル検査ツールSMVを操作することで、より深い理解を得ることができます。
内容のレベル 基礎
講 師 早水 公二(株式会社フォーマルテック)
対 象 一般 ※ 定員 36 名(先着順)
参加費(税込) 一般会員 10,000円、一般非会員 23,000円
学生会員 3,000円、学生非会員 8,000円
※参加費の一部(10%)を、東日本大震災の義援金として寄付いたします。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

 

【TopSEチュートリアル】「分散モデル検証実践」(3/26開催)[終了]

■日 程:2010年3月26日 13:00 ~ 17:30 (受付開始 12:30)
■会 場:国立情報学研究所 20階 講義室1・2(2004,2005)
■参加費:無料

セミナー概要
日 時 2010年3月26日 13:00 ~ 17:30 (受付開始 12:30)
会 場 国立情報学研究所 20階階講義室1・2室(2004,2005)
概 要  モデル検査を現場の問題に適用する際に、検証のための探索空間が巨大になるために、検証が出来ない場合が往々にしてあり、そのための抽象化などの技術が必要になる。しかし、そのための工数が非常にかかり、モデル検査技術の普及を妨げている。本セミナーでは、バックエンドに並列分散計算機環境を利用することで、より大きな検証問題を解くことが可能であることを、演習を通じて経験・理解してもらう。
内容のレベル 応用
講 師 粂野文洋(株式会社三菱総合研究所 情報技術研究センター 主任研究員)
豊嶋大輔(同上)
定 員 20名(先着順)
※NPO法人 トップエスイー教育センターの会員が対象となります。お申込みの際に会員であることをご登録願います。
※GRACEセンター協賛企業の方は事務局までお問い合わせ下さい。
受講料 無料
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

 

【TopSEナイトセミナー】 ソフトウェア工学入門-4日で学ぶソフトウェア工学(2/18, 26, 3/4, 11開催)[終了]

■日 程:
第1夜 2010年 2月18日(木) 17:30-20:40
第2夜 2010年 2月26日(金) 17:30-20:40
第3夜 2010年 3月 4日(木) 17:30-20:40
第4夜 2010年 3月11日(木) 17:30-20:40
■会 場:国立情報学研究所 20階

セミナー概要
日 時 第1夜 2010年 2月18日(木) 17:30-20:40
第2夜 2010年 2月26日(金) 17:30-20:40
第3夜 2010年 3月 4日(木) 17:30-20:40
第4夜 2010年 3月11日(木) 17:30-20:40
会 場 国立情報学研究所 20階
概 要 ソフトウェア工学に関する連続セミナー(4回)を開催します。本セミナーでは、ソフトウェア工学の基本的なトピック(要求分析、設計、プロジェクトマネージメント、形式手法)ごとに専門講師陣が分かりやすく解説します。ソフトウェアにおける要求とは何か?設計をうまく行うにはどうすれば良いか?プロジェクトを円滑に進めるポイントは?フォーマルメソッドとは?など、基礎的な知識を押さえておきたいという方は是非参加ください。完全オムニバス形式ですので、お好きなトピックだけ参加することも可能です。

  • 第1夜 2月18日(木) 17:30-20:40
    • ソフトウェア工学概論 (吉岡 講師, 国立情報学研究所)
    • 要求工学入門 (白銀 講師, 東京女子大)
  • 第2夜 2月26日(金) 17:30-20:40
    • UML入門、アーキテクチャパターンとデザインパターン (鄭 講師, 早稲田大学)
    • 再利用の有用性とプロダクトライン型開発概論 (位野木 講師, 東芝ソリューション)
  • 第3夜 3月 4日(木) 17:30-20:40
    • プロジェクトマネージメント概論 (白川 講師, NTTデータ先端技術)
  • 第4夜 3月11日(木) 17:30-20:40
    • フォーマルメソッド概論(石川講師, 国立情報学研究所)

※本セミナーはトップエスイーの講義ではありませんので、単位は取得できません。

定 員 35名(先着順)
受講料金 一般会員  10,000円
一般非会員 15,000円
学生会員  5,000円
学生非会員 7,000円

※当日会場にて現金でお支払い下さい。領収書を発行します。
※NPO法人 トップエスイー教育センター会員および協力団体の方は「会員」価格となります。
※受講料には教科書代金を含みます。
※国立情報学研究所が主催するトップエスイーに入学予定の受講生の方は無料です。申し込み時にお知らせください。

主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp

【TopSEチュートリアル】「並行システムの検証と実装(入門編)」(12/14開催)[終了]

セミナー概要
日 時 2009年12月14日(月) 10:00~17:00(受付開始:9:30)
会 場 国立情報学研究所 20階 2001A
概 要 本セミナーでは、並行システムの信頼性を高めることを目的として、並行システムをプロセス代数CSP (Communicating Sequential Processes) でモデル化し、モデル検査器FDRで検証し、JavaライブラリJCSPで実装する方法について説明します。CSPは並行システムを解析するための理論、 FDRはCSPモデルを検証するためのツール、JCSPはCSPモデルを並列/分散実行するためのライブラリです。本セミナーの特徴は、CSP理論 →FDR検証→JCSP実装の流れを重視していることにあります。FDRとJCSPの使い方を習得することによって、並行システムのCSPによるモデル化 と検証の考え方をより深く理解することができます。
>■補足情報
講 師 磯部 祥尚(独立行政法人産業技術総合研究所)
定 員 35名(先着順)
受講料金 一般会員  15,000円
一般非会員 25,000円
学生会員  5,000円
学生非会員 8,000円
※当日会場にて現金でお支払い下さい。領収書を発行します。
※「会員」:NPO法人 トップエスイー教育センター会員、NPO法人 CSPコンソーシアム会員、日本ソフトウェア科学会会員が割引の対象となります。
主 催 NPO法人 トップエスイー教育センター
協 力 国立情報学研究所 GRACEセンター
NPO法人 CSPコンソーシアム
日本ソフトウェア科学会 ソフトウェア工学の基礎研究会
お問合せ窓口 セミナーに関するご質問などは、下記アドレスにて承ります。
seminar@topse.or.jp