今回は、並行プロセスの解析や検証ツールの一つとして有名なPAT(プロセス
分析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼び
してリアルタイム性のモデル検査技術の導入から最新動向までを講演して頂き
ます。直接最新のモデル検査ツールが学べるまたとない機会となっています。
また、午後は、NPO法人トップエスイー教育センターが主催のハンズオンセミナー
もございます。ぜひ、そちらもご参加ください。
※今回のセミナーは英語で行われます。
◆◆第73回GRACEセミナー ◆◆
【日時】2014年4月17日（木）10:00-12:00
※午後のハンズオンセミナーの詳細に関しては、以下のトップエスイー教育
センターの案内をご覧下さい。
http://topse.or.jp/2014/03/2186
【会場】国立情報学研究所(NII) 20階 ミーティングルーム１・２(2009,2010)
〒101-8430 東京都千代田区一ツ橋2-1-2
[http://www.nii.ac.jp/about/access/]
【参加費】無料
参加ご希望の方は，下記よりご登録をお願いいたします:
http://form1.fc2.com/form/?id=628975
【お問い合わせ先】
石川冬樹(seminar-steering_AT_grace-center.jp)
_AT_を＠に書き換えてください。
Title: Event Analytics and Verification: The PAT approach
Speaker: Jin Song Dong (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] 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/)
午後には、以下のハンズオンセミナーも開催いたします。
日時：2014年4月17日（木）13:30-16:30
タイトル： PATハンズオン～ふれながら学ぶモデル検査
講師: 藤本 洋 氏(キャッツ(株))
詳細：http://topse.or.jp/2014/03/2186
事前受付：必要
こちらも合わせてご参加下さい。
協力：トップエスイー プロジェクト
