[logic-ml] AIST Seminar on Software Reliability

[山形賴之]

皆様、産総研の山形です。重複して案内を受け取られた方にはお詫びいたします。

下記の内容で、形式手法の実践的な側面に焦点を当てたセミナーを開催いたします。どなたでも参加できますが、参加される方は前日までに山形までご一報下さい。特にお車で参加される方はその旨お伝えください。

Dear everyone, I am pleased to announce "AIST Seminar on Software
Reliability".  This is a seminar on formal methods which is focused on
industrial applications.  The seminar is open to everyone, but
please let me know by 3/19 if you want to join.  In particular, if you
come by a car, please let me know.

AIST Seminar on Software Reliability
date: Mar 20, 2015
Place: National Institute of Advanced Industrial Science and
Technology (AIST), Tsukuba central, AIST Tsukuba Headquarters and
Information Technology Collaborative Research Center
Map: http://www.aist.go.jp/aist_e/guidemap/tsukuba/tsukuba_map.html
http://www.aist.go.jp/aist_e/guidemap/tsukuba/center/tsukuba_map_c.html


14:00 - 14:45 Survey on concurrent model checkers, Yoriyuki Yamagata
14:45 - 15:00 Discussion
15:00 - 15:15 Break
15:15 - 16:00 Using Model Checking and Theorem Proving to Validate and Verify
Cyber-Physical Systems, Chen-wei Wang
16:00 - 16:15 Discussion
16:15 - 16:30 Break
16:30 - 17:15  Applications of Model Checking on Different Systems
using PAT, Liu Yang
17:15 - 17:30 Discussion
18:30 - Dinner

Title: Survey on concurrent model checkers
Speaker: Yoriyuki Yamagata
Abstract:
In this talk, we compare algorithms and performance benchmarks of
concurrent model checkers Spin and LTSmin.  The benchmarks suggests
that LTSmin uses multicore quite efficiently, while Spin is optimized
to singlecore.


Title: Using Model Checking and Theorem Proving to Validate and Verify
Cyber-Physical Systems
Speaker: Chen-wei Wang
Abstract:
In this talk I present part of the results that contribute to the
research project "Certification of Safety-Critical Software-Intensive
Systems" funded by the Ontario government. The project involves
various application domains: biomedical, automotive, and nuclear. This
talk focuses on the nuclear domain. Contributions are made by
researchers at York University and McMaster University. I first
present the use of an automated checking tools for Timed Transition
Models (TTM) to model, simulate, and validate cyber-physical systems,
with respect to discrete-time temporal properties. I then present the
use of tabular expressions and the PVS theorem prover to model and
verify function blocks that can be reused to build Programmable Logic
Controllers (PLCs). In both approaches, I use function blocks supplied
by the industrial standard 61131-3 for illustration. To conclude the
talk, I report lessons that we learn and mention ongoing research.

Title: Applications of Model Checking on Different Systems using PAT
Speaker: Liu Yang
Abstract:
Model checking is emerging as an effective software verification
method with wide applications. However, still there are a lot research
challenges in model checking techniques and in applying model checking
techniques. To address these challenges, this talk presents our recent
research contributions in the system modeling, efficient model
checking algorithms development and the application of formal
verification in concurrent objects design, cyber physical systems,
security, multi-agent systems and pervasive systems. More important,
we introduce a process analysis toolkit (PAT,www.patroot.com), which
is a self-contained verification framework for specification,
simulation and verification of concurrent, real-time and probabilistic
systems. Since PAT is released 8 years ago, it has attracted 3500+
registered users world wide. Our vision is to achieve pervasive model
checking so as to build a framework for realizing different
verification techniques, and making model checking as planning,
problem-solving, scheduling/services.

Short Bio: Dr Liu Yang graduated in 2005 with a Bachelor of Computing
(Honours) in the National University of Singapore (NUS). In 2010, he
obtained his PhD and started his post doctoral work in NUS, MIT and
SUTD. In 2011, Dr Liu is awarded the Temasek Research Fellowship at
NUS to be the Principal Investigator in the area of Cyber Security. In
2012 fall, he joined School of Computer Engineering, Nanyang
Technological University as a Nanyang Assistant professor.

Dr. Liu specializes in software verification, security and software
engineering. His research has bridged the gap between the theory and
practical usage of formal methods to evaluate the design and
implementation of software for high assurance. His work led to the
development of a state-of-the-art model checker, Process Analysis
Toolkit (PAT). This tool is used by research institutions in over 70
countries for research and education. He has more than 100
publications and leading a research group of 30 people.

--
山形頼之
独立行政法人 産業技術総合研究所 主任研究員
https://staff.aist.go.jp/yoriyuki.yamagata/