A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear sy...A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear symbolic LFT model of the UAV is derived in a standard M-A form where M represents the nominal, known, part of the system and A contains the time-varying, uncertain and nonlinear components. The advantages of the proposed modeling approach are that： it not only provides an ideal starting point to obtain various final design-oriented models through subse- quent assumptions and simplifications, but also it facilitates the control system analysis with models of different levels of fidelity/complexity. Furthermore, a linearized symbolic LFT model of the UAV is proposed based on the LFT differentiation, which is amenable directly to a sophisticated linear ro- bust control strategy such as μ synthesis/analysis. Both of the derived LFT models are validated with the original nonlinear model in time domain. Simulation results show the effectiveness of the pro- posed algorithm.展开更多
To apply the fire modelling for the fire engineer with symbolic mathematics,the key equations of a zone model were demonstrated. There were thirteen variables with nine constraints,so only four ordinary differential e...To apply the fire modelling for the fire engineer with symbolic mathematics,the key equations of a zone model were demonstrated. There were thirteen variables with nine constraints,so only four ordinary differential equations (ODEs) were required to solve. A typical fire modelling with two-room structure was studied. Accordingly,the source terms included in the ODEs were simplified and modelled,and the fourth Runge-Kutta method was used to solve the ordinary differential equations (ODEs) with symbolic mathematics. Then a zone model could be used with symbolic mathematics. It is proposed that symbolic mathematics is possible for use by fire engineer.展开更多
A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiat...A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.展开更多
The present study aims at improving the ability of the canonical genetic programming algorithm to solve problems, and describes an improved genetic programming (IGP). The proposed method can be described as follows: t...The present study aims at improving the ability of the canonical genetic programming algorithm to solve problems, and describes an improved genetic programming (IGP). The proposed method can be described as follows: the first inves-tigates initializing population, the second investigates reproduction operator, the third investigates crossover operator, and the fourth investigates mutation operation. The IGP is examined in two domains and the results suggest that the IGP is more effective and more efficient than the canonical one applied in different domains.展开更多
Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is f...Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.展开更多
Symbolic circuit simulator is traditionally applied to the small-signal analysis of analog circuits. This paper establishes a symbolic behavioral macromodeling method applicable to both small-signal and large-signal a...Symbolic circuit simulator is traditionally applied to the small-signal analysis of analog circuits. This paper establishes a symbolic behavioral macromodeling method applicable to both small-signal and large-signal analysis of general two-stage operational amplifiers （op-amps）. The proposed method creates a two-pole parametric macromodel whose parameters are analytical functions of the circuit element parameters generated by a symbolic circuit simulator. A moment matching technique is used in deriving the analytical model parameter. The created parametric behavioral model can be used for op-amps performance simulation in both frequency and time domains. In particular, the parametric models are highly suited for fast statistical simulation of op-amps in the time-domain. Experiment results show that the statistical distributions of the op-amp slew and settling time characterized by the proposed model agree well with the transistor-level results in addition to achieving significant speedup.展开更多
A numerical model and transmission characteristic analysis of DPSK （differential phase shift keying） pressure signals in mud channels is introduced. With the control logic analysis of the rotary valve mud telemetry,...A numerical model and transmission characteristic analysis of DPSK （differential phase shift keying） pressure signals in mud channels is introduced. With the control logic analysis of the rotary valve mud telemetry, a logical control signal is built from a Gate function sequence according to the binary symbols of transmitted data and a phase-shift function is obtained by integrating the logical control signal. A mathematical model of the DPSK pressure signal is built based on principles of communications by modulating carrier phase with the phase-shift function and a numerical simulation of the pressure wave is implemented with the mathematical model by MATLAB programming. Considering drillpipe pressure and drilling fluid temperature profile along drillpipes, the drillpipe of a vertical well is divided into a number of sections. With water-based drilling fluids, the impacts of travel distance, carrier frequency, drillpipe size, and drilling fluids on the signal transmission were studied by signal transmission characteristic analysis for all the sections. Numerical calculation results indicate that the influences of the viscosity of drilling fluids and volume fraction of gas in drilling fluids on the DPSK signal transmission are more notable than the others and the signal will distort in waveform with differential attenuations of the signal frequent component.展开更多
GPU (Graphics Processing Unit) is used in various areas. Therefore, the demand for the verification of GPU programs is increasing. In this paper, we suggest the method to detect bank conflict by using symbolic executi...GPU (Graphics Processing Unit) is used in various areas. Therefore, the demand for the verification of GPU programs is increasing. In this paper, we suggest the method to detect bank conflict by using symbolic execution. Bank conflict is one of the bugs happening in GPU and it leads the performance of programs lower. Bank conflict happens when some processing units in GPU access the same shared memory. Symbolic execution is the method to analysis programs with symbolic values. By using it, we can detect bank conflict on GPU programs which use many threads. We implement a prototype of the detector for bank conflict and evaluate it with some GPU programs. The result states that we can detect bank conflict on the programs with no loop regardless of the number of threads.展开更多
文摘A nonlinear modeling framework is presented for an oceanographic unmanned aerial vehicle （UAV） by using symbolic modeling and linear fractional transformation （LFT） techniques . Consequently, an exact nonlinear symbolic LFT model of the UAV is derived in a standard M-A form where M represents the nominal, known, part of the system and A contains the time-varying, uncertain and nonlinear components. The advantages of the proposed modeling approach are that： it not only provides an ideal starting point to obtain various final design-oriented models through subse- quent assumptions and simplifications, but also it facilitates the control system analysis with models of different levels of fidelity/complexity. Furthermore, a linearized symbolic LFT model of the UAV is proposed based on the LFT differentiation, which is amenable directly to a sophisticated linear ro- bust control strategy such as μ synthesis/analysis. Both of the derived LFT models are validated with the original nonlinear model in time domain. Simulation results show the effectiveness of the pro- posed algorithm.
基金Project(PolyU B-Q01e) supported by the Research Project "Onsetting of Internal Fire Whirls in Buildings and Associated Safet Provision"
文摘To apply the fire modelling for the fire engineer with symbolic mathematics,the key equations of a zone model were demonstrated. There were thirteen variables with nine constraints,so only four ordinary differential equations (ODEs) were required to solve. A typical fire modelling with two-room structure was studied. Accordingly,the source terms included in the ODEs were simplified and modelled,and the fourth Runge-Kutta method was used to solve the ordinary differential equations (ODEs) with symbolic mathematics. Then a zone model could be used with symbolic mathematics. It is proposed that symbolic mathematics is possible for use by fire engineer.
基金Supported by the Natural Science Foundation of Guizhou Province(No.20050119)the Natural Science Foundation of Guizhou Education(No.2004219)
文摘A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects- non-repudiation and fairness using SME. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker.
文摘The present study aims at improving the ability of the canonical genetic programming algorithm to solve problems, and describes an improved genetic programming (IGP). The proposed method can be described as follows: the first inves-tigates initializing population, the second investigates reproduction operator, the third investigates crossover operator, and the fourth investigates mutation operation. The IGP is examined in two domains and the results suggest that the IGP is more effective and more efficient than the canonical one applied in different domains.
文摘Debugging software code has been a challenge for software developers since the early days of computer programming. A simple need, because the world is run by software. So perhaps the biggest engineering challenge is finding ways to make software more reliable. This review provides an overview of techniques developed over time in the field of software model checking to solve the problem of detecting errors in program code. In addition, the challenges posed by this technology are discussed and ways to mitigate them in future research and applications are proposed. A comprehensive examination of the various model verification methods used to detect program code errors is intended to lay the foundation for future research in this area.
文摘Symbolic circuit simulator is traditionally applied to the small-signal analysis of analog circuits. This paper establishes a symbolic behavioral macromodeling method applicable to both small-signal and large-signal analysis of general two-stage operational amplifiers （op-amps）. The proposed method creates a two-pole parametric macromodel whose parameters are analytical functions of the circuit element parameters generated by a symbolic circuit simulator. A moment matching technique is used in deriving the analytical model parameter. The created parametric behavioral model can be used for op-amps performance simulation in both frequency and time domains. In particular, the parametric models are highly suited for fast statistical simulation of op-amps in the time-domain. Experiment results show that the statistical distributions of the op-amp slew and settling time characterized by the proposed model agree well with the transistor-level results in addition to achieving significant speedup.
基金supported by High Technology Research and Development Program of China(No.2006AA06A101).
文摘A numerical model and transmission characteristic analysis of DPSK （differential phase shift keying） pressure signals in mud channels is introduced. With the control logic analysis of the rotary valve mud telemetry, a logical control signal is built from a Gate function sequence according to the binary symbols of transmitted data and a phase-shift function is obtained by integrating the logical control signal. A mathematical model of the DPSK pressure signal is built based on principles of communications by modulating carrier phase with the phase-shift function and a numerical simulation of the pressure wave is implemented with the mathematical model by MATLAB programming. Considering drillpipe pressure and drilling fluid temperature profile along drillpipes, the drillpipe of a vertical well is divided into a number of sections. With water-based drilling fluids, the impacts of travel distance, carrier frequency, drillpipe size, and drilling fluids on the signal transmission were studied by signal transmission characteristic analysis for all the sections. Numerical calculation results indicate that the influences of the viscosity of drilling fluids and volume fraction of gas in drilling fluids on the DPSK signal transmission are more notable than the others and the signal will distort in waveform with differential attenuations of the signal frequent component.
文摘GPU (Graphics Processing Unit) is used in various areas. Therefore, the demand for the verification of GPU programs is increasing. In this paper, we suggest the method to detect bank conflict by using symbolic execution. Bank conflict is one of the bugs happening in GPU and it leads the performance of programs lower. Bank conflict happens when some processing units in GPU access the same shared memory. Symbolic execution is the method to analysis programs with symbolic values. By using it, we can detect bank conflict on GPU programs which use many threads. We implement a prototype of the detector for bank conflict and evaluate it with some GPU programs. The result states that we can detect bank conflict on the programs with no loop regardless of the number of threads.
