Speaker:	Ji Wang , National University of Defense Technology
Period:	2009-04-30 16:00 ~ 2009-04-30 17:00
Place:	Room 308, Bldg 302, SNU

Abstract

PSL is a specification language which has been accepted as an industrial standard. In PSL, SEREs are used as additional formula constructs. We present a variant of PSL, namely APSL, which replaces SEREs with finite automata. APSL and PSL are of the exactly same expressiveness. Then, we extend the LTL symbolic model checking algorithm to that of APSL, and then present a tableau based APSL verification technique, which can be implemented via BDD based symbolic approach. Moreover, we implement an extension of NuSMV, which supports symbolic model checking of APSL. The experimental results show that APSL can be efficiently verified.

Short bio

Prof. Ji Wang received his B.S., M.S. and Ph.D. in Computer Science from National University of Defense Technology in 1987, 1990 and 1995 respectively. Since 2002, he is a full professor in School of Computer of National University of Defense Technology. His research interest includes formal analysis and verification of software systems, programming methodology for distributed computing. As principal investigator, he has been awarded more than 10 projects funded by National Grand Basic Research Programme (973), National Hi-Tech Research and Development Programme (863), and National Natural Science Foundation of China etc. He is deputy director of National Laboratory for Parallel and Distributed Processing of China since 2007. In 2007, he has won National Science Fund for Distinguished Young Scholars of China.

Resources

• talk slide