GRACEメールマガジン2014/4/7 第39号

◆□◆GRACEメールマガジン2014/4/7 第39号◆□◆



主催: NII 先端ソフトウェア工学国際研究センター(GRACEセンター)
協力:トップエスイー プロジェクト

国立情報学研究所(NII) 20階 ミーティングルーム1・2(2009,2010)


析ツール)の提案者、Jin-Song Dong博士(シンガポール国立大学)をお呼びして



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. (

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.


タイトル: PATハンズオン~ふれながら学ぶモデル検査
講師: 藤本 洋 氏(キャッツ(株))



●GRACEメールマガジンの 第34号をお届けしました。
ご意見、ご感想は、GRACEセンター事務局 (


カテゴリー: メルマガ パーマリンク