Many websites use verification codes to prevent users from using the machine automatically to register,login,malicious vote or irrigate but it brought great burden to the enterprises involved in internet marketing as ...Many websites use verification codes to prevent users from using the machine automatically to register,login,malicious vote or irrigate but it brought great burden to the enterprises involved in internet marketing as entering the verification code manually.Improving the verification code security system needs the identification method as the corresponding testing system.We propose an anisotropic heat kernel equation group which can generate a heat source scale space during the kernel evolution based on infinite heat source axiom,design a multi-step anisotropic verification code identification algorithm which includes core procedure of building anisotropic heat kernel,settingwave energy information parameters,combing outverification codccharacters and corresponding peripheral procedure of gray scaling,binarizing,denoising,normalizing,segmenting and identifying,give out the detail criterion and parameter set.Actual test show the anisotropic heat kernel identification algorithm can be used on many kinds of verification code including text characters,mathematical,Chinese,voice,3D,programming,video,advertising,it has a higher rate of 25%and 50%than neural network and context matching algorithm separately for Yahoo site,49%and 60%for Captcha site,20%and 52%for Baidu site,60%and 65%for 3DTakers site,40%,and 51%.for MDP site.展开更多
The virtual machine of code mechanism (VMCM) as a new concept for code mechanical solidification and verification is proposed and can be applied in MEMS (micro-electromechanical systems) security device for high c...The virtual machine of code mechanism (VMCM) as a new concept for code mechanical solidification and verification is proposed and can be applied in MEMS (micro-electromechanical systems) security device for high consequence systems. Based on a study of the running condition of physical code mechanism, VMCM's configuration, ternary encoding method, running action and logic are derived. The cases of multi-level code mechanism are designed and verified with the VMCM method, showing that the presented method is effective.展开更多
The immersed boundary method is an effective technique for modeling and simulating fluid-structure interactions especially in the area of biomechanics.This paper analyzes the accuracy of the immersed boundary method.T...The immersed boundary method is an effective technique for modeling and simulating fluid-structure interactions especially in the area of biomechanics.This paper analyzes the accuracy of the immersed boundary method.The procedure contains two parts,i.e.,the code verification and the accuracy analysis.The code verification provides the confidence that the code used is free of mistakes,and the accuracy analysis gives the order of accuracy of the immersed boundary method.The method of manufactured solutions is taken as a means for both parts.In the first part,the numerical code employs a second-order discretization scheme,i.e.,it has second-order accuracy in theory.It matches the calculated order of accuracy obtained in the numerical calculation for all variables.This means that the code contains no mistake,which is a premise of the subsequent work.The second part introduces a jump in the manufactured solution for the pressure and adds the corresponding singular forcing terms in the momentum equations.By analyzing the discretization errors,the accuracy of the immersed boundary method is proven to be first order even though the discretization scheme is second order.It has been found that the coarser mesh may not be sensitive enough to capture the influence of the immersed boundary,and the refinement on the Lagrangian markers barely has any effect on the numerical calculation.展开更多
Previous analytical results on flow splitting are generalized to consider multiple boiling channels systems. The analysis is consistent with the approximations usually adopted in the use of systems codes (like RELAP5 ...Previous analytical results on flow splitting are generalized to consider multiple boiling channels systems. The analysis is consistent with the approximations usually adopted in the use of systems codes (like RELAP5 and TRACE5, among others) commonly applied to perform safety analyses of nuclear power plants. The problem is related to multiple, identical, parallel boiling channels, connected through common plena. A theoretical model limited in scope explains this flow splitting without reversal. The unified analysis performed and the confirmatory computational results found are summarized in this paper. New maps showing the zones where this behavior is predicted are also shown considering again twin pipes. Multiple pipe systems have been found not easily amenable for analytical analysis when dealing with more than four parallel pipes. However, the particular splitting found (flow along N pipes dividing in one standalone pipe flow plus N -1 identical pipe flows) has been verified up to fourteen pipes, involving calculations in systems with even and odd number of pipes using the RELAP5 systems thermal-hydraulics code.展开更多
Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this pap...Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.展开更多
Embedded RAM blocks(BRAMs) in field programmable gate arrays(FPGAs) are susceptible to single event effects(SEEs) induced by environmental factors such as cosmic rays, heavy ions, alpha particles and so on. As t...Embedded RAM blocks(BRAMs) in field programmable gate arrays(FPGAs) are susceptible to single event effects(SEEs) induced by environmental factors such as cosmic rays, heavy ions, alpha particles and so on. As technology scales, the issue will be more serious. In order to tackle this issue, two different error correcting codes(ECCs), the shortened Hamming codes and shortened BCH codes, are investigated in this paper. The concrete design methods of the codes are presented. Also, the codes are both implemented in flash-based FPGAs. Finally, the synthesis report and simulation results are presented in the paper. Moreover, heavy-ion experiments are performed,and the experimental results indicate that the error cross-section of the device using the shortened Hamming codes can be reduced by two orders of magnitude compared with the device without mitigation, and no errors are discovered in the experiments for the device using the shortened BCH codes.展开更多
Accurate prediction of the sawtooth cycle[1]is an important test for nonlinear MHD codes.The sawtooth cycle in the CDX-U tokamak[2],chosen because its small size and low temperature allow simulation using actual devic...Accurate prediction of the sawtooth cycle[1]is an important test for nonlinear MHD codes.The sawtooth cycle in the CDX-U tokamak[2],chosen because its small size and low temperature allow simulation using actual device parameters,has been an important benchmark for the comparison of theM3D[3]and NIMROD[5]codes for the last several years.Successive comparisons have led to improvements and refinements in both codes.The most recent comparisons show impressive agreement between the two codes both on the linear instability and on the details of nonlinear cyclical behavior.These tests are somewhat idealized and do not yet agree quantitatively with the experimentally observed sawtooth period.We expect a second generation of CDX-U sawtooth benchmarks based on an analytically specified equilibrium,with source terms that show greater fidelity to the physical device,to produce better agreement.展开更多
基金The national natural science foundation(61273290,61373147)Xiamen Scientific Plan Project(2014S0048,3502Z20123037)+1 种基金Fujian Scientific Plan Project(2013HZ0004-1)FuJian provincial education office A-class project(-JA13238)
文摘Many websites use verification codes to prevent users from using the machine automatically to register,login,malicious vote or irrigate but it brought great burden to the enterprises involved in internet marketing as entering the verification code manually.Improving the verification code security system needs the identification method as the corresponding testing system.We propose an anisotropic heat kernel equation group which can generate a heat source scale space during the kernel evolution based on infinite heat source axiom,design a multi-step anisotropic verification code identification algorithm which includes core procedure of building anisotropic heat kernel,settingwave energy information parameters,combing outverification codccharacters and corresponding peripheral procedure of gray scaling,binarizing,denoising,normalizing,segmenting and identifying,give out the detail criterion and parameter set.Actual test show the anisotropic heat kernel identification algorithm can be used on many kinds of verification code including text characters,mathematical,Chinese,voice,3D,programming,video,advertising,it has a higher rate of 25%and 50%than neural network and context matching algorithm separately for Yahoo site,49%and 60%for Captcha site,20%and 52%for Baidu site,60%and 65%for 3DTakers site,40%,and 51%.for MDP site.
基金Project supported by High-Technology Research and Develop-ment Program of China (Grant No .863 -2003AA404210)
文摘The virtual machine of code mechanism (VMCM) as a new concept for code mechanical solidification and verification is proposed and can be applied in MEMS (micro-electromechanical systems) security device for high consequence systems. Based on a study of the running condition of physical code mechanism, VMCM's configuration, ternary encoding method, running action and logic are derived. The cases of multi-level code mechanism are designed and verified with the VMCM method, showing that the presented method is effective.
基金supported by the National Natural Science Foundation of China (No 10472070)
文摘The immersed boundary method is an effective technique for modeling and simulating fluid-structure interactions especially in the area of biomechanics.This paper analyzes the accuracy of the immersed boundary method.The procedure contains two parts,i.e.,the code verification and the accuracy analysis.The code verification provides the confidence that the code used is free of mistakes,and the accuracy analysis gives the order of accuracy of the immersed boundary method.The method of manufactured solutions is taken as a means for both parts.In the first part,the numerical code employs a second-order discretization scheme,i.e.,it has second-order accuracy in theory.It matches the calculated order of accuracy obtained in the numerical calculation for all variables.This means that the code contains no mistake,which is a premise of the subsequent work.The second part introduces a jump in the manufactured solution for the pressure and adds the corresponding singular forcing terms in the momentum equations.By analyzing the discretization errors,the accuracy of the immersed boundary method is proven to be first order even though the discretization scheme is second order.It has been found that the coarser mesh may not be sensitive enough to capture the influence of the immersed boundary,and the refinement on the Lagrangian markers barely has any effect on the numerical calculation.
文摘Previous analytical results on flow splitting are generalized to consider multiple boiling channels systems. The analysis is consistent with the approximations usually adopted in the use of systems codes (like RELAP5 and TRACE5, among others) commonly applied to perform safety analyses of nuclear power plants. The problem is related to multiple, identical, parallel boiling channels, connected through common plena. A theoretical model limited in scope explains this flow splitting without reversal. The unified analysis performed and the confirmatory computational results found are summarized in this paper. New maps showing the zones where this behavior is predicted are also shown considering again twin pipes. Multiple pipe systems have been found not easily amenable for analytical analysis when dealing with more than four parallel pipes. However, the particular splitting found (flow along N pipes dividing in one standalone pipe flow plus N -1 identical pipe flows) has been verified up to fourteen pipes, involving calculations in systems with even and odd number of pipes using the RELAP5 systems thermal-hydraulics code.
基金This work was supported by the National Natural Science Foundation of China under Grant No.61632005.
文摘Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.
基金Supported by National Natural Science Foundation of China(11079045,11179003 and 11305233)
文摘Embedded RAM blocks(BRAMs) in field programmable gate arrays(FPGAs) are susceptible to single event effects(SEEs) induced by environmental factors such as cosmic rays, heavy ions, alpha particles and so on. As technology scales, the issue will be more serious. In order to tackle this issue, two different error correcting codes(ECCs), the shortened Hamming codes and shortened BCH codes, are investigated in this paper. The concrete design methods of the codes are presented. Also, the codes are both implemented in flash-based FPGAs. Finally, the synthesis report and simulation results are presented in the paper. Moreover, heavy-ion experiments are performed,and the experimental results indicate that the error cross-section of the device using the shortened Hamming codes can be reduced by two orders of magnitude compared with the device without mitigation, and no errors are discovered in the experiments for the device using the shortened BCH codes.
基金Cal-culations were performed at the National Energy Research Scientific Computing Center(NERSC)which is supported by the Office of Science of the U.S.Department of Energy under Contract No.DE-AC02-05CH11231,and at the National Center for Computational Sciences(NCCS)This work was performed under Grants No.DE-AC02-76CH03073 and DE-FC02-02ER54668 with the U.S.Department of Energy.
文摘Accurate prediction of the sawtooth cycle[1]is an important test for nonlinear MHD codes.The sawtooth cycle in the CDX-U tokamak[2],chosen because its small size and low temperature allow simulation using actual device parameters,has been an important benchmark for the comparison of theM3D[3]and NIMROD[5]codes for the last several years.Successive comparisons have led to improvements and refinements in both codes.The most recent comparisons show impressive agreement between the two codes both on the linear instability and on the details of nonlinear cyclical behavior.These tests are somewhat idealized and do not yet agree quantitatively with the experimentally observed sawtooth period.We expect a second generation of CDX-U sawtooth benchmarks based on an analytically specified equilibrium,with source terms that show greater fidelity to the physical device,to produce better agreement.