A secure operating system in the communication network can provide the stable working environment,which ensures that the user information is not stolen.The micro-kernel operating system in the communication network re...A secure operating system in the communication network can provide the stable working environment,which ensures that the user information is not stolen.The micro-kernel operating system in the communication network retains the core functions in the kernel,and unnecessary tasks are implemented by calling external processes.Due to the small amount of code,the micro-kernel architecture has high reliability and scalability.Taking the microkernel operating system in the communication network prototype VSOS as an example,we employ the objdump tool to disassemble the system source code and get the assembly layer code.On this basis,we apply the Isabelle/HOL,a formal verification tool,to model the system prototype.By referring to the mathematical model of finite automata and taking the process scheduling module as an example,the security verification based on the assembly language layer is developed.Based on the Hoare logic theory,each assembly statement of the module is verified in turn.The verification results show that the scheduling module of VSOS has good functional security,and also show the feasibility of the refinement framework.展开更多
This paper presents a fourth-order Cartesian grid based boundary integral method(BIM)for heterogeneous interface problems in two and three dimensional space,where the problem interfaces are irregular and can be explic...This paper presents a fourth-order Cartesian grid based boundary integral method(BIM)for heterogeneous interface problems in two and three dimensional space,where the problem interfaces are irregular and can be explicitly given by parametric curves or implicitly defined by level set functions.The method reformulates the governing equation with interface conditions into boundary integral equations(BIEs)and reinterprets the involved integrals as solutions to some simple interface problems in an extended regular region.Solution of the simple equivalent interface problems for integral evaluation relies on a fourth-order finite difference method with an FFT-based fast elliptic solver.The structure of the coefficient matrix is preserved even with the existence of the interface.In the whole calculation process,analytical expressions of Green’s functions are never determined,formulated or computed.This is the novelty of the proposed kernel-free boundary integral(KFBI)method.Numerical experiments in both two and three dimensions are shown to demonstrate the algorithm efficiency and solution accuracy even for problems with a large diffusion coefficient ratio.展开更多
Finite-frequency travel time tomography is a newly developing method.The main procedure in this new method is to compute the traveltime sensitive kernel.The travel time of the same scatterer needs to be used for compu...Finite-frequency travel time tomography is a newly developing method.The main procedure in this new method is to compute the traveltime sensitive kernel.The travel time of the same scatterer needs to be used for computing the traveltime sensitive kernel many times.It is a time-consuming task.It is easy and fast to get the travel time from analytic equations in a simple model such as a homogenous or linear velocity media.However,most of the earth models are layered.It is cumbersome to get the travel time from analytic equations.In order to enhance the computation efficiency,we used the table look-up method to compute the finite-frequency travel time sensitive kernel for P-waves in a layered structure model.We chose the AK135 earth model for the velocity model.The table look-up method saved about 50% of the computation time.We enhanced the computation speed by using the table lookup method in the same velocity model,which was very useful for enhancing the computation efficiency for the finite-frequency travel time tomography.展开更多
Hydraulic fracturing （HF） technique has been extensively used for the exploitation of unconventional oiland gas reservoirs. HF enhances the connectivity of less permeable oil and gas-bearing rock formationsby fluid ...Hydraulic fracturing （HF） technique has been extensively used for the exploitation of unconventional oiland gas reservoirs. HF enhances the connectivity of less permeable oil and gas-bearing rock formationsby fluid injection, which creates an interconnected fracture network and increases the hydrocarbonproduction. Meanwhile, microseismic （MS） monitoring is one of the most effective approaches to evaluatesuch stimulation process. In this paper, the combined finite-discrete element method （FDEM） isadopted to numerically simulate HF and associated MS. Several post-processing tools, includingfrequency-magnitude distribution （b-value）, fractal dimension （D-value）, and seismic events clustering,are utilized to interpret numerical results. A non-parametric clustering algorithm designed specificallyfor FDEM is used to reduce the mesh dependency and extract more realistic seismic information.Simulation results indicated that at the local scale, the HF process tends to propagate following the rockmass discontinuities; while at the reservoir scale, it tends to develop in the direction parallel to themaximum in-situ stress. 2014 Institute of Rock and Soil Mechanics, Chinese Academy of Sciences. Production and hosting byElsevier B.V. All rights reserved.展开更多
Provides information on a study which presented a numerical method for solving Euler system of equations in reproducing kernel space. Definition and properties of reproducing kernel space; Construction of reproducing ...Provides information on a study which presented a numerical method for solving Euler system of equations in reproducing kernel space. Definition and properties of reproducing kernel space; Construction of reproducing kernel finite difference method; Numerical results of the study.展开更多
基金This work was supported in part by the Natural Science Foundation of Jiangsu Province under grant No.BK20191475the fifth phase of“333 Project”scientific research funding project of Jiangsu Province in China under grant No.BRA2020306the Qing Lan Project of Jiangsu Province in China under grant No.2019.
文摘A secure operating system in the communication network can provide the stable working environment,which ensures that the user information is not stolen.The micro-kernel operating system in the communication network retains the core functions in the kernel,and unnecessary tasks are implemented by calling external processes.Due to the small amount of code,the micro-kernel architecture has high reliability and scalability.Taking the microkernel operating system in the communication network prototype VSOS as an example,we employ the objdump tool to disassemble the system source code and get the assembly layer code.On this basis,we apply the Isabelle/HOL,a formal verification tool,to model the system prototype.By referring to the mathematical model of finite automata and taking the process scheduling module as an example,the security verification based on the assembly language layer is developed.Based on the Hoare logic theory,each assembly statement of the module is verified in turn.The verification results show that the scheduling module of VSOS has good functional security,and also show the feasibility of the refinement framework.
基金the National Natural Science Foundation of China(Grant No.DMS-12101553,Grant No.DMS-11771290)the Natural Science Foundation of Zhejiang Province(Grant No.LQ22A010017)+4 种基金the National Key Research and Development Program of China(Project No.2020YFA0712000)the Science Challenge Project of China(Grant No.TZ2016002)the Strategic Priority Research Program of Chinese Academy of Sciences(Grant No.XDA25000400)the National Science Foundation of America(Grant No.ECCS-1927432)also partially supported by the National Science Foundation of America(Grant No.DMS-1720420).
文摘This paper presents a fourth-order Cartesian grid based boundary integral method(BIM)for heterogeneous interface problems in two and three dimensional space,where the problem interfaces are irregular and can be explicitly given by parametric curves or implicitly defined by level set functions.The method reformulates the governing equation with interface conditions into boundary integral equations(BIEs)and reinterprets the involved integrals as solutions to some simple interface problems in an extended regular region.Solution of the simple equivalent interface problems for integral evaluation relies on a fourth-order finite difference method with an FFT-based fast elliptic solver.The structure of the coefficient matrix is preserved even with the existence of the interface.In the whole calculation process,analytical expressions of Green’s functions are never determined,formulated or computed.This is the novelty of the proposed kernel-free boundary integral(KFBI)method.Numerical experiments in both two and three dimensions are shown to demonstrate the algorithm efficiency and solution accuracy even for problems with a large diffusion coefficient ratio.
基金supported by the National Natural Science Foundation of China (Grant No. 90814013)
文摘Finite-frequency travel time tomography is a newly developing method.The main procedure in this new method is to compute the traveltime sensitive kernel.The travel time of the same scatterer needs to be used for computing the traveltime sensitive kernel many times.It is a time-consuming task.It is easy and fast to get the travel time from analytic equations in a simple model such as a homogenous or linear velocity media.However,most of the earth models are layered.It is cumbersome to get the travel time from analytic equations.In order to enhance the computation efficiency,we used the table look-up method to compute the finite-frequency travel time sensitive kernel for P-waves in a layered structure model.We chose the AK135 earth model for the velocity model.The table look-up method saved about 50% of the computation time.We enhanced the computation speed by using the table lookup method in the same velocity model,which was very useful for enhancing the computation efficiency for the finite-frequency travel time tomography.
基金supported by the Natural Sciences and Engineering Research Council of Canada through Discovery Grant 341275 (G. Grasselli) and Engage EGP 461019-13
文摘Hydraulic fracturing （HF） technique has been extensively used for the exploitation of unconventional oiland gas reservoirs. HF enhances the connectivity of less permeable oil and gas-bearing rock formationsby fluid injection, which creates an interconnected fracture network and increases the hydrocarbonproduction. Meanwhile, microseismic （MS） monitoring is one of the most effective approaches to evaluatesuch stimulation process. In this paper, the combined finite-discrete element method （FDEM） isadopted to numerically simulate HF and associated MS. Several post-processing tools, includingfrequency-magnitude distribution （b-value）, fractal dimension （D-value）, and seismic events clustering,are utilized to interpret numerical results. A non-parametric clustering algorithm designed specificallyfor FDEM is used to reduce the mesh dependency and extract more realistic seismic information.Simulation results indicated that at the local scale, the HF process tends to propagate following the rockmass discontinuities; while at the reservoir scale, it tends to develop in the direction parallel to themaximum in-situ stress. 2014 Institute of Rock and Soil Mechanics, Chinese Academy of Sciences. Production and hosting byElsevier B.V. All rights reserved.
基金NSFC and Project (HIT 2000.01) supported by the Scientific ResearchFoundation of Harbin institute of Technology.
文摘Provides information on a study which presented a numerical method for solving Euler system of equations in reproducing kernel space. Definition and properties of reproducing kernel space; Construction of reproducing kernel finite difference method; Numerical results of the study.
