Dear everyone, (apologies for multiple posts)

I am pleased to announce another TSSS at AIST Tsukuba central, held Mar. 23, 2015. The program is as follows. Note that the largest canteen in AIST Tsukuba central is closed, so we have a long lunch break. You can eat and drink in the seminar room.

The seminar is open to everyone, but please let me know by Mar. 19 if you want to attend. In particular, if you come by car, please let me know.

皆様、(重複投稿をお許し下さい)

2015年3月23日に産総研のつくばセンターでTSSSを開催いたします。プログラムは下記のとおりです。どなたでも参加できますが、参加予定の方はあらかじめ3月19日までに山形までご一報下さい。特にお車でお越しになる方は連絡をお願いします。

なお、産総研の大食堂は現在閉鎖中です。外に食事に行けるよう昼休みを長めにとっています。セミナー室は飲食可能です。

よろしくお願いします。

Tsukuba Software Science Seminar

Date: Mar. 23, 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

10:00 - 10:45 Runtime verification using a process algebra CSP, Yoriyuki Yamagata 10:45 - 11:00 Discussion 11:00 - 13:00 Break 13:00 - 13:45 Applying Formal Methods in Trust and Security systems, Liu Yang 13:45 - 14:00 Discussion 14:00 - 14:15 Break 14:15 - 15:00 Using Model Checking and Theorem Proving to Validate and Verify Cyber-Physical Systems, Chen-wei Wang 15:00 - 15:15 Discussion

Title: Speaker: Yoriyuki Yamagata Abstract: A process algebra such as CSP, CCS, and pi-calculus is used to describe a concurrent system. In this talk, we introduce a tool called CSP_E, CSP for event monitoring. CSP_E tests a runtime log against a specification given by CSP, and report whether the log satisfies the given specification or not. CSP_E is implemented as a internal DSL within Scala programming language.

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: Applying Formal Methods in Trust and Security systems Speaker: Liu Yang Abstract: Cyber-attack detection, defense and recovery are important topics in cybersecurity, but the ultimate goal of cybersecurity is to build attack-free systems. Security verification and building attack-free systems are very challenging tasks in view of the size and the complexity of the systems. In this talk, we will present our recent attempts in applying formal methods in modeling and verifying security protocols, security protocol implementations, malware in Android OS and even vulnerabilities. We will also discuss the challenges in applying formal methods in security and possible solutions. Lastly, we will introduce our recent research project “Securify: A Compositional Approach of Building Security Verified System”, which aims at building secure and verifiable systems ground-up.

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/