Seminars

An Online Finite LTL Model Checker for Distributed Systems (PDF file)
Zhengwei Qi, Associate Professor, Shanghai Jiao Tong University-Shanghai, China

05/20/2011, 2pm GHC-6501

Abstract

Modern software model checkers are usually used to find safety violations. However, checking liveness properties can offer a more natural and effective way to detect errors, particularly in complex concurrent and distributed e-business systems. Specifying global liveness properties which should always eventually be true proves to be more desirable, but it is hard for existing software model checkers to verify liveness in real codes because doing so requires finding an infinite execution. For solving such a challenge, we proposes an online model checker to verify the safety and liveness properties of complex systems. We adopt the linear temporal logic to describe the semantics of the finite model checking, use binary instrumentation to obtain the distribute states and apply a checking engine to dynamically verify the finite trace linear temporal logic properties. At last, we demonstrate the method in a distributed system using distributed protocol Paxos and achieve good results by experiments. Additionally, I will give a brief introduction about our system related research projects in SJTU.

Biography

Zhengwei QI received a B.Eng degree from Northwestern Polytechnical University, in 1999, a M.Eng degree in Computer Science from the same university, in 2002, and a Ph.D. degree in Computer Science from Shanghai Jiao Tong University, under the supervision of Prof. Jinyuan You , in 2005. After receiving his Ph.D., he taught in the School of Software, Shanghai Jiao Tong University, up to now.

Dr. QI leads the System Group in School of Software, SJTU. His research interests are static/dynamic program analysis, model checking, virtual machines, and distributed systems. He has achieved the National Natural Science Foundation of China (NSFC 2008 and 2010). From January to July of 2008, he focused on the LTL based dynamic program analysis as a visiting teacher in the system group of Microsoft Research Asia. Now he is a visiting scholar in CMU SCS, hosted by Professor Edmund M. Clarke.