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 existi...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.展开更多
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 wh...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.展开更多
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 wit...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.展开更多
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 morph...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.展开更多
Semantic secure communication is an emerging field that combines the principles of source-channel coding with the need for secure data transmission.It is of great significance in modern communications to protect the c...Semantic secure communication is an emerging field that combines the principles of source-channel coding with the need for secure data transmission.It is of great significance in modern communications to protect the confidentiality and privacy of sensitive information and prevent information leaks and malicious attacks.This paper presents a novel approach to semantic secure communication through the utilization of joint source-channel coding,which is based on the design of an automated joint source-channel coding algorithm and an encryption and decryption algorithm based on semantic security.The traditional and state-of-the-art joint source-channel coding algorithms are selected as two baselines for different comparison purposes.Experimental results demonstrate that our proposed algorithm outperforms the first baseline algorithm,the traditional source-channel coding,by 61.21%in efficiency under identical channel conditions(SNR=15 dB).In security,our proposed method can resist 2 more types of attacks compared to the two baselines,exhibiting nearly no increases in time consumption and error rate compared to the state-of-the-art joint source-channel coding algorithm while the secure semantic communication is supported.展开更多
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 in...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.展开更多
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 c...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.展开更多
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 ...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.展开更多
Gust fronts,which are characterized by strong winds and intense wind shear,pose a threat to both aviation and public safety.To aid forecasters in issuing timely warnings for this hazardous weather phenomenon,a deep le...Gust fronts,which are characterized by strong winds and intense wind shear,pose a threat to both aviation and public safety.To aid forecasters in issuing timely warnings for this hazardous weather phenomenon,a deep learning-based automatic gust front identification algorithm is proposed in this study.The algorithm utilizes Mask Region-based Convolutional Neural Network(Mask R-CNN),a state-of-the-art instance segmentation model,trained on a large dataset of 2623 gust front samples from S-band weather radar volume scans in East China and the North China Plain between 2009 and 2016.Extensive data preprocessing and manual annotation are performed to prepare the training dataset.The optimized model achieves impressive performance on a test set of 604 samples,with a detection probability of 93.21%,a false alarm rate of 3.60%,a missed alarm rate of 6.79%,and a critical success index of 90.08%.The algorithm demonstrates robust identification capabilities across gust fronts of varying scales,types,and parent thunderstorm systems,highlighting its operational applicability.展开更多
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 huma...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.展开更多
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 cryptana...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.展开更多
基金Supported by the National Natural Science Foundation of China(61862033,61902162)Key Project of Science and Technology Research of Department of Education of Jiangxi Province(GJJ210307)Postgraduate Innovation Fund Project of Education Department of Jiangxi Province(YC2021-S306)。
文摘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.
文摘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.
基金Supported by the 863 Programof China (2001AA242111)
文摘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.
基金Supported by the National Natural Science Foundation of China(59975035,41006058)the Fundamental Research Funds for the Central Universities(2014212020205)
文摘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.
基金supported in part by the National Key R&D Program of China under Grant 2022YFB3103500in part by the National Natural Science Foundation of China under Grant 62302195.
文摘Semantic secure communication is an emerging field that combines the principles of source-channel coding with the need for secure data transmission.It is of great significance in modern communications to protect the confidentiality and privacy of sensitive information and prevent information leaks and malicious attacks.This paper presents a novel approach to semantic secure communication through the utilization of joint source-channel coding,which is based on the design of an automated joint source-channel coding algorithm and an encryption and decryption algorithm based on semantic security.The traditional and state-of-the-art joint source-channel coding algorithms are selected as two baselines for different comparison purposes.Experimental results demonstrate that our proposed algorithm outperforms the first baseline algorithm,the traditional source-channel coding,by 61.21%in efficiency under identical channel conditions(SNR=15 dB).In security,our proposed method can resist 2 more types of attacks compared to the two baselines,exhibiting nearly no increases in time consumption and error rate compared to the state-of-the-art joint source-channel coding algorithm while the secure semantic communication is supported.
文摘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.
基金This research was supported by the Excellent Young Teachers Program of the Ministry of Education, P. R. China, the National Natural Science Foundation of China(No. 60375010)
文摘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.
基金the National Natural Science Foundation of China(No.61976091)。
文摘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.
基金Supported by the National Key Research and Development Program of China(2023YFC3007501)Open Fund of China Meteorological Administration Key Laboratory for Aviation Meteorology(HKQXZ-2024005)Innovation Ability Promotion Plan of Chengdu University of Information Technology(KYQN202307).
文摘Gust fronts,which are characterized by strong winds and intense wind shear,pose a threat to both aviation and public safety.To aid forecasters in issuing timely warnings for this hazardous weather phenomenon,a deep learning-based automatic gust front identification algorithm is proposed in this study.The algorithm utilizes Mask Region-based Convolutional Neural Network(Mask R-CNN),a state-of-the-art instance segmentation model,trained on a large dataset of 2623 gust front samples from S-band weather radar volume scans in East China and the North China Plain between 2009 and 2016.Extensive data preprocessing and manual annotation are performed to prepare the training dataset.The optimized model achieves impressive performance on a test set of 604 samples,with a detection probability of 93.21%,a false alarm rate of 3.60%,a missed alarm rate of 6.79%,and a critical success index of 90.08%.The algorithm demonstrates robust identification capabilities across gust fronts of varying scales,types,and parent thunderstorm systems,highlighting its operational applicability.
文摘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.
基金This work was supported by the National Natural Science Foundation of China(Grant No.61872359,62122085 and 61936008)the National Key R&D Program of China(Grant No.2020YFB1805402),and the Youth Innovation Promotion Association of Chinese Academy of Sciences.
文摘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.
