WEN Xinxiu, received her M.S. degree in computer science from Jilin University, China in 2003. She is now a Ph.D. candidate in the Department of Com- puter Science and Engineering, East China University of Science and Technology, China. Her main research interests include software architecture, and forma~ methods. Email: wenxinxiu@ecust.edu.cn YU Huiqun, received his MS. degree in computer science from East China University of Science and Technology (ECUST), China in 1992, his Ph.D. degree in computer science from Shanghai Jiao Tong Univer- sity, China in 1995. He is now a Professor in the Dep- artment of Computer Science and Engineering, ECUST, China. His research interests include information security, software architecture, and formal methods. *The corresponding author. Email: yhq@ecust.edu.cn ZHENG Hong, received her Ph.D. degree in computer software and theory from Chinese Academy of Sci- ence, China in 2003. She joined East China University of Science and Technology, China in 2003, where she is currently an Associate Professor in the Department of the Computer Science and Engineering. She is a visiting scholar with the Department of Computer Science and Engineering, University of California, USA. Her research interests include pervasive computing, system modelling and analysis, context-aware. Email: zhenghong@ecust.edu.cn