Automatic Algorithm Programming Model Based on the Improved Morgan's Refinement Calculus

The automatic algorithm programming model can increase the dependability and efficiency of algorithm program development,including specification generation,program refinement,and formal verification.However,the existing model has two flaws:incompleteness of program refinement and inadequate automation of formal verification.This paper proposes an automatic algorithm programming model based on the improved Morgan’s refinement calculus.It extends the Morgan’s refinement calculus rules and designs the C++generation system for realizing the complete process of refinement.Meanwhile,the automation tools VCG(Verification Condition Generator)and Isabelle are used to improve the automation of formal verification.An example of a stock’s maximum income demonstrates the effectiveness of the proposed model.Furthermore,the proposed model has some relevance for automatic software generation.

An Incremental Approach to Automatic Algorithm Design

This paper presents an incremental approach to automatic algorithm design, which can be described by algebraic specifications precisely and conveniently. The definitions of selection operator and extension operator which can bedefined by strategy relations and transformations are given in order to model theprocess of finding the solution of a problem. Also discussed is its object-orientedimplementation. The functional specification and the design specification for an algorithm are given in one framework so that the correctness of the algorithm can beeasily proved.

Algorithm of Dynamic Operation Process of Hydraulic Automatically Operated Canals with Constant-Downstream Level Gates

On the basis of analysis the governing process of downstream water level gates AVIO and AVIS, a mathematical model for simulation of dynamic operation process of hydraulically automated irrigation canals instalIed with AVIO and AVIS gates is presented, the main point of this rnathematical model is firstly applying a set of unsteady flow equations （St. Venant equations here） and treating the condition of gate movement as its dynamic boundary, and then deeoupling this interaction of gate movement with the change of canal flow. In this process, it is necessary to give the gateg open-loop transfer function whose input is water level deviation and output is gate discharge. The result of this simulation for a practical reach has shown it has satisfactory accuracy.

Which is the Best PID Variant for Pneumatic Soft Robots?An Experimental Study

This paper presents an experimental study to compare the performance of model-free control strategies for pneumatic soft robots.Fabricated using soft materials,soft robots have gained much attention in academia and industry during recent years because of their inherent safety in human interaction.However,due to structural flexibility and compliance,mathematical models for these soft robots are nonlinear with an infinite degree of freedom(DOF).Therefore,accurate position(or orientation)control and optimization of their dynamic response remains a challenging task.Most existing soft robots currently employed in industrial and rehabilitation applications use model-free control algorithms such as PID.However,to the best of our knowledge,there has been no systematic study on the comparative performance of model-free control algorithms and their ability to optimize dynamic response,i.e.,reduce overshoot and settling time.In this paper,we present comparative performance of several variants of model-free PID-controllers based on extensive experimental results.Additionally,most of the existing work on modelfree control in pneumatic soft-robotic literature use manually tuned parameters,which is a time-consuming,labor-intensive task.We present a heuristic-based coordinate descent algorithm to tune the controller parameter automatically.We presented results for both manual tuning and automatic tuning using the Ziegler-Nichols method and proposed algorithm,respectively.We then used experimental results to statistically demonstrate that the presented automatic tuning algorithm results in high accuracy.The experiment results show that for soft robots,the PID-controller essentially reduces to the PI controller.This behavior was observed in both manual and automatic tuning experiments;we also discussed a rationale for removing the derivative term.

A novel algorithm for automatic localization of human eyes

Based on geometrical facial features and image segmentation, we present a novel algorithm for automatic localization of human eyes in grayscale or color still images with complex background. Firstly, a determination criterion of eye location is established by the prior knowledge of geometrical facial features. Secondly, a range of threshold values that would separate eye blocks from others in a segmented face image (i.e., a binary image) are estimated. Thirdly, with the progressive increase of the threshold by an appropriate step in that range, once two eye blocks appear from the segmented image, they will be detected by the determination criterion of eye location. Finally, the 2D correlation coefficient is used as a symmetry similarity measure to check the factuality of the two detected eyes. To avoid the background interference, skin color segmentation can be applied in order to enhance the accuracy of eye detection. The experimental results demonstrate the high efficiency of the algorithm and correct localization rate.

Real-Time Automatic Scaling Method of Oblique Ionogram Parameters Based on Morphological Operator and Inversion Technique

Automatic scaling ionogram can get the parameters of ionogram which are vital to ionosphere detecting. In this paper, a new method is proposed to scale F2 layer trace automatically from oblique ionogram based on morphological operator and inversion technique. This method is verified through the comparison of actual detecting data with statistical analysis. The results show that the proposed automatic scaling method has high acceptable rate and is suitable for scaling oblique ionogram with different high angle wave states. It is fast and precise to fit O-mode echoes in F2 layer without the influence from F1 layer. This method could be applied in real-time ionospheric oblique sounding research with high reliability and versatility.

Gaussian Mixture Statistics Model Based on Automatic Inspection System Used in ITS

The ITS is becoming more and more important in the economic development of China. But most of the ITS used in Chinese major cities need the human to perform the supervision task. As a result, it consumes too much human resources, and also can not achieve the satisfied supervision performance. Thus, in this paper, we will propose an automatic inspection system based on the Gaussian mixture statistics model to alleviate this kind of problem. The proposed method will utilize a Gaussian Mixture model to model the background, and then use the EM algorithm to update the model＇s coefficients frame by frame to make the model adapt to the changing environment. After successful modeling, we can extract out the foreground blocks from background blocks, and finally trigger the automatic alarming system by calculating the number of foreground blocks. From the experiment results, our proposed method can achieve considerable good results.

Improved conditional differential attacks on lightweight hash family QUARK

Nonlinear feedback shift register(NFSR)is one of the most important cryptographic primitives in lightweight cryptography.At ASIACRYPT 2010,Knellwolf et al.proposed conditional differential attack to perform a cryptanalysis on NFSR-based cryptosystems.The main idea of conditional differential attack is to restrain the propagation of the difference and obtain a detectable bias of the difference of the output bit.QUARK is a lightweight hash function family which is designed by Aumasson et al.at CHES 2010.Then the extended version of QUARK was published in Journal of Cryptology 2013.In this paper,we propose an improved conditional differential attack on QUARK.One improvement is that we propose a method to select the input difference.We could obtain a set of good input differences by this method.Another improvement is that we propose an automatic condition imposing algorithm to deal with the complicated conditions efficiently and easily.It is shown that with the improved conditional differential attack on QUARK,we can detect the bias of output difference at a higher round of QUARK.Compared to the current literature,we find a distinguisher of U-QUARK/D-QUARK/S-QUARK/C-QUARK up to 157/171/292/460 rounds with increasing 2/5/33/8 rounds respectively.We have performed the attacks on each instance of QUARK on a 3.30 GHz Intel Core i5 CPU,and all these attacks take practical complexities which have been fully verified by our experiments.As far as we know,all of these results have been the best thus far.

USSL Net:Focusing on Structural Similarity with Light U-Structure for Stroke Lesion Segmentation

Automatic segmentation of ischemic stroke lesions from computed tomography(CT)images is of great significance for identifying and curing this life-threatening condition.However,in addition to the problem of low image contrast,it is also challenged by the complex changes in the appearance of the stroke area and the difficulty in obtaining image data.Considering that it is difficult to obtain stroke data and labels,a data enhancement algorithm for one-shot medical image segmentation based on data augmentation using learned transformation was proposed to increase the number of data sets for more accurate segmentation.A deep convolutional neural network based algorithm for stroke lesion segmentation,called structural similarity with light U-structure(USSL)Net,was proposed.We embedded a convolution module that combines switchable normalization,multi-scale convolution and dilated convolution in the network for better segmentation performance.Besides,considering the strong structural similarity between multi-modal stroke CT images,the USSL Net uses the correlation maximized structural similarity loss(SSL)function as the loss function to learn the varying shapes of the lesions.The experimental results show that our framework has achieved results in the following aspects.First,the data obtained by adding our data enhancement algorithm is better than the data directly segmented from the multi-modal image.Second,the performance of our network model is better than that of other models for stroke segmentation tasks.Third,the way SSL functioned as a loss function is more helpful to the improvement of segmentation accuracy than the cross-entropy loss function.