中文摘要：

Zheng WANG received his BS in Soft- ware Engineering and PhD in Com- puter applied technique from East China Normal University. Now he is a soflware requirement engineer in the Software Development Department at Beijing Institute of Control Engineer- ing, China Academy of Space Technol- ogy. His main research topic focuses onthe automatization and formalization of requirement analysis lbr embedded control software. His work also relates with automatic test case generation E-mail： ggpu@sei.ecnu.edu.cnGeguang PU holds a PhD in mathe- matics from Peking University, Bei- jing, China. Currently, he works as an associate professor at Software Engi- neering Institute of East China Normal University, Shanghai, China. His re- search interests include program anal- ysis, formal modeling of business pro- cesses, automated testing, and veri-tication. From 2006, he served as PC members in a number of international academic conferences, including ICFEM10]I 1, UTP10/I 1/12. ICTACI2 etc. Recently Dr. Pu uses the lightweight formal model to analyze timed-driven control software, including requirement analysis and automated test data generation. Jianwen LI is a PhD graduate student supervised by Jifeng HE and Geguang PU in East China Normal University. Now he is in University Rice as a visit- ing student. His research topics are LTL model checking, automata theory, and data flow analysis. Yuxiang CHEN is a MS graduate stu- dent supervised by Jifeng HE and Geguang PU in East China Normal University. His research topics are re- quirement analysis and automatic test- ing. Yongxin ZHAO holds a PhD in tech- nology of computer application from East China Normal University. He is a research fellow at School of Com- puting of National University of Sin- gapore, Singapore. His research inter- ests include program analysis and veri- fication, semantics theory, web services and formal methods and he owns morethan 15 referred publications. Mingsong CHEN received the BS and ME from Department of Computer Sci- ence and Technology, Nanjin