[logic-ml] TSSS (Tsukuba Software Science Seminar) at AIST Tsukuba, Mar. 23, 2015

[山形賴之]

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/