กก

Research Projects Overview

 

   I had nearly 3 years experience in scheduling problems research, especially in solving the job-shop problem for Harbin Electromotor Factory. Then I was awarded excellent master thesis in Harbin Science and Technology University. During my master candidate time, I designed and implemented an algorithm based on efficiency function for job-shop problem, whose efficiency was shown by the comparing with other methods in practice. Besides, I also devised an optimal genetic algorithm for the same problem, in which a new encode rule and genetic operators were proposed and corresponding global convergence was proved.

My research during Ph.D candidate concentrated on formal methods research including model checking and automatic verification for distributed systems, especially in Grid computing environment. During my Ph.D. candidate time in Shanghai Jiaotong University (visiting student in Lab. of Computer Science, Institute of Software, Chinese Academy of Sciences), I have given a formal model based on Spin/Promela to describe some critical components of Grid computing environment such as Grid Directory Service and Grid Security Architecture, which is the first attempt of exploiting formal model to describe such components of Grid Computing system. Based on the formal model, I have developed an algorithm for automatic verification for such distributed/concurrent systems. In order to avoid state explosion, I presented an abstract method to simulate the parameterized system (one of infinite state systems) and developed a verification algorithm based on constraint programming, which was implemented with C++ under UNIX. Because testing method seems necessary to remove the suspicion of correctness of such formal models, I developed a tool for automatic generating feasible test cases from SDL. With our tool, the feasibility of generated test cases are certainly sure, for which the constraint solving strategy is adopted. After many experiments, I concluded that in Grid computing environment, formal verification method is efficient for some critical components; abstract technique is necessary for some homogenous large scaled components such as MPP computer, and testing is important for large scaled heterogeneous components.

My contribution, as a postdoctoral researcher in LIX Ecole Polytechnique France, is formal framework and an implementation that allow us to compute a description of the complexity of a given MiniML program. As an operational semantics of a program, its complexity should be compositional. This leads to decorate the rules describing the operational semantics of MiniML by some complexity information that will then allow to compute variables (or parameters), the complexity depends of course on the value of these variables. In case these variables are higher-order, it also depends from the complexity of the actual functions that will instantiate these variables. For such programs, our method generates a symbolic description of this complexity, which can be hopefully transformed into a more convenient format: recurrence relations. This method is partly implemented in OCaml.

I presented a first step of a project of automatic complexity analysis for programs extracted from coq proofs. I implemented a tool, which makes the generation of the recurrence equations in the case of functions on natural numbers and functions on lists whose recursive schema is recursive primitive (possibly of higher type). The recurrence equations generators is not yet linked to a computer algebra system to analyze them.