並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼びしてリアルタイム性のモデル検査のチュートリアル、および、ハンズオンセミナーを開催いたします。第１部は、ツールの 提案者から直接最新のモデル検査ツールが学べるまたとない機会となっています。また第２部では、実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法、時間制約表現の機能など学べます。ぜひこの機会にお誘いあわせの上、ご参加ください。
■プログラム：
13:30-15:00 第１部：Event-Strategy Analytics: The PAT approach
講演者：Jin-Song Dong 准教授, The National University of Singapore
15:10-17:00 第２部：PATハンズオン〜PATによるモデリングとモデル検査の実際〜
講師: 藤本 洋 氏(イーソル株式会社技術本部)
※注意：第１部は英語での講演となります（通訳なし）。
※第２部の演習のため、以下の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/)
=== 第２部: PATハンズオン 〜PATによるモデリングとモデル検査の実際～
時間：15:10-17:00
講師: 藤本 洋 氏(イーソル株式会社 技術本部)
[概要]
本セミナーでは、プロセス代数(CSP)に基づくモデル検査ツールPAT (Process Analysis Toolkit)の基本的な使い方を理解します。実際にツールを使って頂きながら、PATを利用したモデルの作成方法、シミュレーション方法、検査方法を解説します。
[講師プロフィール]
電気通信大学電気通信学研究科博士前期課程(情報工学）修了。専門は数理モデリング、ソフトウェア開発。経験分野は銀行系(第三次オンライン）、ICカードシステム、物理現象のシミュレーションと可視化、医療系システム、セマンティックWebシステム、車載ネットワーク、形式手法ツールの導入支援、マルチ・メニーコア上で動作するの並列処理ソフトウェア開発支援環境研究開発。現在、イーソル株式会社技術本部所属。エキスパート職。日本PATユーザ会。
