タグ: モデル検査

※注意：午前の第１部は英語での講演となります（通訳なし）。また午前の部のみの参加は無料です。
※ 午後の部は会場に用意されたシンクライアントを使って演習を行います。ご自身の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/
)
=== 第２部: PATハンズオン～ふれながら学ぶモデル検査～
時間：13:30-16:30
講師: 藤本 洋 氏(キャッツ(株))

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

■プログラム：
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カードシステム、電子手帳組み込みの ソフト、物理現象のシミュレーションと可視化、医療系システム、車載ネットワーク、モデル変換など。現職ではツール開発と形式手法ツールを担当する。現在、キャッツ株式会社　プロダクト事業本部 技術企画第２グループ　技術マネージャ。

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