Title: Combining Model Checking and Testing with an Application to Reliability Prediction and Distribution.主讲人：Dr. Liu Yang时间：2014 年 5 月 29 日（周四）上午 10:30地点：软件楼第二会议室abstract:
Testing provides a probabilistic assurance of system correctness. In general, testing relies on the assumptions that the system under test is deterministic so that test cases can be sampled. However, a challenge arises when a system under test behaves non-deterministiclly in a dynamic operating environment because it will be unknown how to sample test cases. In this work, we propose a method combining hypothesis testing and probabilistic model checking so as to provide the "assurance" and quantify the error bounds. The idea is to apply hypothesis testing to deterministic system components and use probabilistic model checking techniques to lift the results through non-determinism. Furthermore, if a requirement on the level of assurance" is given, we apply probabilistic model checking techniques to push down therequirement through non-determinism to individual components so that they can be verified using hypothesis testing. We motivate and demonstrate our method through an application of system reliability prediction and distribution. Our approach has been realized in a toolkit named RaPiD, which has been applied to investigate two real-world systems.
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 an assistant professor. Dr. Liu specializes in software verification using model checking techniques. 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 50 countries for research and education.
