並行プロセスの解析や検証ツールの一つとして有名な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ハンズオン～ふれながら学ぶモデル検査
講師: 藤本 洋 氏(キャッツ(株))
※注意：午前の第１部は英語での講演となります（通訳なし）
※ 午後の部は会場に用意されたシンクライアントを使って演習を行います。ご自身の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カードシステム、電子手帳組み込みの ソフト、物理現象のシミュレーションと可視化、医療系システム、車載ネットワーク、モデル変換など。現職ではツール開発と形式手法ツールを担当する。現在、キャッツ株式会社 プロダクト事業本部 技術企画第２グループ 技術マネージャ。
|
