講演会のお知らせ
Yoriyuki Yamagata
モデル検査器PATおよび仕様記述言語Bメソッドの開発者の方が関西に来られて講演されます。平日になってしまいますが、お越しいただければ幸いです。
なお、参加予定の方は予め北村崇師 <t.kit...@aist.go.jp>まで連絡をとって頂くようお願いします。
---------------------------------------------------------------
日時：平成 23 年 11 月 28 日（月） 13：30--15: 00
場所：（独）産総研関西センター尼崎事業所 E 棟 2 階 セミナー室
http://cfv.jp/cvs/access/index.html
演題：Pervasive Model Checking
講演者：Dr. LIU, Yang
(Senior Research Scientist, National University of Singapore)
梗概：:
Model checking is emerging as an effective software verification method.
In this talk, we introduce a process analysis toolkit (PAT, www.patroot.com),
which is a self-contained verification system for system specification,
simulation and verification. PAT supports a wide range of modeling
languages for concurrent and real-time systems, probabilistic systems,
web services, sensor network, distributes systems and so on. Furthermore,
PAT has an extensible and integrated architecture to support the
development of model checkers for wide range application domains. PAT
adopts a layered design with an intermediate representation layer (IRL),
which separates modeling languages from model checking algorithms so
that the algorithms can be shared by different languages. IRL contains
several common semantic models to support wide application domains, and
builds both explicit model checking and symbolic model checking under
one roof. PAT architecture provides extensibility in many possible
aspects: modeling languages, model checking algorithms, reduction
techniques and even IRLs. Various model checkers have been developed
under this new architecture in months time. Our vision is to achieve
pervasive model checking, i.e., model checking as planning, problem-solving,
scheduling/services. Since PAT is released 4 years ago, it has attracted
1500+ registered users world wide, specially with a Japanese user group.
---------------------------------------------------------------
日時：平成 23 年 12 月 2 日（金） 16：00--18: 00
場所：（独）産総研関西センター尼崎事業所 E 棟 2 階 セミナー室
http://cfv.jp/cvs/access/index.html
講演者：Alexei Iliasov, Ilya Lopatkin and Alexander Romanovsky
(School of Computing Science, Newcastle University, UK)
演題：Scaling Event-B to Industrial Applications
梗概：
This talk reports on our work in a major EC FP7 integrated
project DEPLOY on industrial deployment of system engineering methods
providing high dependability and productivity. This 4-year project (*
http://www.deploy-project.eu/* <http://www.deploy-project.eu/>) ends in
April 2012. The overall aim of DEPLOY is to make major advances in
engineering methods for dependable systems through the deployment of formal
methods. The deployment is mainly targeting companies from the automotive,
aerospace, transportation and business information sectors. The Newcastle
team coordinates this project and is involved in its all major activities,
including method and tool development, as well as technology transfer. In
the talk we will outline the project, report on our experience in
industrial deployment of formal methods and tools, and present our results
on developing methods and tools supporting safety analysis and fault
tolerance, and assisting system certification. The talk will include
several demos of the tools developed as part of the Rodin toolset (
http://www.event-b.org/).
--
山形頼之
(独)産業技術総合研究所 研究員
E-mail: yoriyuki...@aist.go.jp
http://staff.aist.go.jp/yoriyuki.yamagata/