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

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

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/