Li TAN

My primary research interests are in the areas of formal verification, specifically in program and software systems verification by applying formal methods to software engineering, like model checking, situation calculus, OCL, etc.

I am an M.S. student working with Prof. Zongyuan Yang. Prior to being a master student, I received my B.S. Degree with distinction in Computer Science from East China Normal University, Shanghai, China, and got Graduate Entrance Examination waived out of 121. At present, I endeavor to achieve my M.S Degree supposed to be finished in two and a half years only in two years before further Ph.D. career.

I have already graduated from ECNU and I really enjoy the 6 years of being an ECNUer. Thank you, all friends! See you in 4 years.

Education

• B.S. in Computer Science, 09/2004 - 06/2008
  East China Normal University, Shanghai, China
  Thesis: "Ajax based Real-Time Teaching Website for the Course 'Principles of Compiler'". (Abstract) (Website)
  Advisor: Prof. Zongyuan Yang

• M.S. in Computer Science, 09/2008 - 06/2010
  East China Normal University, Shanghai, China
  Thesis: "A Research of UML Formal Verification Based on Situation Calculus and OCL Constraints Automatic Generation". (Abstract) (Prototype Tool Snapshot)
  Advisor: Prof. Zongyuan Yang

Publications

• Journal Papers:
  
  
  • Li Tan, Zongyuan Yang and Jinkui Xie. "Data Response Optimization of the Ajax Technology" (in Chinese), in Journal of Computer Engineering, Vol. 36, No. 7, pp. 52-54, 2010.
  To summarize an optimized model of Ajax which is more efficient and secure, this paper analyzes the work principle and data transmission performance of Ajax, and then discusses the difference between XML and JSON by experiments with a focus on the format of response data returned. Furthermore, some suggestions for choosing either based on the current application scenarios are given, which improves the shortcomings such as data response redundancy caused by Ajax nowadays.
  
  
  • Li Tan, Jinxia Xie and Lei A. "Using Multiple Regression Analysis in the Prediction of Urban Employment in China" (in Chinese), submitted to Journal of Numerical Methods and Computer Applications, withdrawn.
  This paper compares incremental sum of squares of regression of influential factors of urban employment in China with each other by according data analysis and statistics tools, and then concludes the degree of influence of these factors. Based on multiple regression analysis and Trend Extrapolation, linear multiple regression model is founded and checked. Furthermore, this model is refined by industries, regions and employment establishments. Considering relevant national policies and plans, prediction of urban employment in China in 2009 and 2010 is made. Finally, according to the importance of influential factors and current social condition, possible extension of the model and suggestions of solving urban employment problem are given.


• Conference and Workshop Papers:
  
  
  • Li Tan, Zongyuan Yang and Jinkui Xie. "UCVSC: A Formal Approach to UML Class Diagram Online Verification Based on Situation Calculus", in Proceedings of the 4th International Conference on Computer Sciences and Convergence Information Technology (ICCIT'09), pp. 375-380, Seoul, Korea, Nov. 2009.
  The gap between informal models used in a UML environment and formal verifications and proofs in academic research prevents UML from valid and efficient application. In this paper, we propose an approach to bridge the gap between UML class diagram and situation calculus via our formal verification tool, UCVSC (UML Class diagram online Verification based on Situation Calculus). UML class diagram describes a software system informally while situation calculus is employed as the underlying formalism to precisely specify the system. With respect to most components in UML class diagram, the strength of reasoning about actions and describing the state of the world in situation calculus can be applied to represent them appropriately. Using UML tools and predefined mapping mechanism, we transform UML class diagram to XMI, an intermediate format, and finally to situation calculus in Prolog syntax. This approach attempts to provide precise semantics of UML class diagram which can be logically verified. In addition, we automate the verification process in an online prototype system. Furthermore, a case study on an academic system is presented to illustrate and evaluate our approach.
  
  
  • Li Tan, Zongyuan Yang and Jinkui Xie. "OCL Constraints Automatic Generation for UML Class Diagram", in Proceedings of the International Conference on Software Engineering and Service Science (ICSESS’10), pp. ?-?, Beijing, China, July 2010.
  As a standard modeling language of software architecture design, UML lacks formal semantics on account of its informal graphical notation. To further provide refined description of UML, OCL is primarily and widely employed. Generally, OCL constraints are written manually, which may cause incorrectness and extra overhead. Therefore, generating OCL constraints template for UML models is a superior solution. The OCL constraints template automatically generated can be used as a reference for software designers. First of all, the significance of automatic generation of OCL constraints was emphasized, and then the application domain of OCL was shown, followed by a lexical analysis of how to extract the target objects in UML models where OCL constraints were needed to build and an algorithm of extraction. Eventually, this extraction algorithm was implemented by Perl. In our way, the overall quality and efficiency of software design is enhanced and thus contributions are made for the automation of Software Engineering.
  
  
  • Li Tan, Zongyuan Yang and Jinkui Xie. "Verifying UML in Prolog", submitted to the 10th International Conference on Formal Methods in Computer Aided Design (FMCAD’10), Lugano, Switzerland, Oct. 2010.
  From the viewpoint of software life cycle in Software Engineering, software architecture is the core of the structure and behavior of software. As software architecture design itself is a kind of modeling activity, how to verify the correctness of the standard modeling language of software architecture design, UML, is one big problem. This paper used the implementation of situation calculus, Prolog, to describe a subset of UML diagrams, a graphic notation formally and evaluate it an equivalent formal semantics. Then we verified possible syntax and semantic errors in UML in a Prolog interpreter, SWI-Prolog, after a definition of error types in UML. Finally, a goal was achieved that software designers could correct the design of UML diagrams prior to fixing bugs in code in the phase of test, which avoided unnecessary system overhead in the following phases of Software Engineering with the hope of enhancing the overall efficiency of the process of Software Engineering.
  
  

Research

• Situation Calculus Based UML Class & State Diagram Online Verification System
  • proposed a formal mapping mechanism of verifying UML class and state diagram by situation calculus to prevent ambiguous interpretation occurred in UML, the informal graphic notation;
  • developed an online verification tool by Perl with the help of XMI, an intermediate format;
  • employed a Prolog interpreter, SWI-prolog to verify the previous modeling, and thus helped developers find and correct design flaws, if any;
  • proposed an algorithm of OCL constraints template automatic generation for UML class diagram, which focused on how to extract targets of OCL constraints from UML models.
• Ajax Data Response Optimization Project
  • analyzed the working principle and data transmission performance of Ajax;
  • discussed the difference between two common formats of response data returned, XML and JSON, by experiments with a focus on the aspects of data amount, parsing efficiency of client, developing efficiency of server and security.

Released Tools

• USCVSC: An online tool for UML Class & State diagram Verification based on Situation Calculus

Industrial Experience

• ASP.NET Web Developer, Gaotime Co., Ltd., Shanghai, China, May - July 2010
• ASP & PHP Web Developer, University Website Editorial Office, ECNU, Feb. 2009 - June. 2010
• Intel C/C++ Compiler Document Translator, SinoBot Inc., Shanghai, China, July - Aug. 2008
• Windows System Management Engineer, Xinmin Evening Paper, Shanghai, China, July - July 2008
• Research Intern as a Unix System Management Engineer, eBay Inc. China Operation Center, Shanghai, China, July 2007 - Jan. 2008
• ASP Web Developer, Firstlat Info. & Tech. Co., Ltd., Shanghai, China, July - July 2007

Teaching

• Junior course "Principles of Compiler", Feb. - July 2009
• Senior course "Practice in Principles of Compiler", Sep. 2008 - Jan. 2009