Table of Content

25 July 2024, Volume 2024 Issue 4 Previous Issue    Next Issue

For Selected:

Download Citations EndNote Reference Manager ProCite BibTeX RefWorks

Toggle Thumbnails

Computer Science

Select

A formal verification method for embedded operating systems Yang WANG, Jingcheng FANG, Xiong CAI, Zhipeng ZHANG, Yong CAI, Weikai MIAO 2024, 2024 (4):  1-17.  doi: 10.3969/j.issn.1000-5641.2024.04.001 Abstract ( 216 )   HTML ( 13 )   PDF (1364KB) ( 255 )   Save The operating system is the core and foundation of the entire computer system. Its reliability and safety are vital because faults or vulnerabilities in the operating system can lead to system crashes, data loss, privacy breaches, and security attacks. In safety-critical systems, any errors in the operating system can result in significant loss of life and property. Ensuring the safety and reliability of the operating system has always been a major challenge in industry and academia. Currently, methods for verifying the operating system’s safety include software testing, static analysis, and formal methods. Formal methods are the most promising in ensuring the operating system’s safety and trustworthiness. Mathematical models can be established using formal methods, and the system can be formally analyzed and verified to discover potential errors and vulnerabilities. In the operating system, formal methods can be used to verify the correctness and completeness of the operating system’s functions and system safety. A formal scheme for embedded operating systems is proposed herein on the basis of existing formal verification achievements for operating systems. This scheme uses VCC (verified C compiler), CBMC (C bounded model checker), and PAT (process analysis toolkit) tools to verify the operating system at the unit, module, and system levels, respectively. The schema, upon being successfully applied to a task scheduling architecture case of a certain operating system, exhibits a certain universality for analyzing and verifying embedded operating systems. Figures and Tables | References | Related Articles | Metrics

Select

Machine-learning-based model checker performance prediction Chengyu ZHANG, Jiayi ZHU, Yihao HUANG, Di YANG, Jianwen LI, Weikai MIAO, Di YAN, Bin GU, Naijun ZHAN, Geguang PU 2024, 2024 (4):  18-29.  doi: 10.3969/j.issn.1000-5641.2024.04.002 Abstract ( 127 )   HTML ( 10 )   PDF (2393KB) ( 102 )   Save An and-inverter graph (AIG) is a representation of electrical circuits typically passed as input into a model checker. In this paper, we propose an AIG structural encoding that we use to extract the features of AIGs and construct a portfolio-based model checker called Liquid. The underlying concept of the proposed structural encoding is the enumeration of all possible AIG substructures, with the frequency of each substructure encoded as a feature vector for use in subsequent machine-learning processes. Because the performance of model-checking algorithms varies across different AIGs, Liquid combines multiple such algorithms and selects the algorithm appropriate for a given AIG via machine learning. In our experiments, Liquid outperformed all state-of-the-art model checkers in the portfolio, achieving a high prediction accuracy. We further studied the effectiveness of Liquid from several perspectives. Figures and Tables | References | Related Articles | Metrics

Physics and Electronics

Select

Impact of ATLAS 2.76 TeV inclusive jet experimental data on CT18NNLO parton distribution functions Ying XU, Honghao FAN, Sayipjamal DULAT 2024, 2024 (4):  30-39.  doi: 10.3969/j.issn.1000-5641.2024.04.003 Abstract ( 74 )   HTML ( 5 )   PDF (1182KB) ( 31 )   Save This study aimed to investigate the impact of the inclusive jet double differential cross-section data retrieved from the ATLAS at the large hadron collider(LHC), at the center-of-mass energy of $ \sqrt{s}=2.76 $ TeV, on CT18NNLO parton distribution functions(PDFs) by applying the error PDF updating method package(ePump). First, the inclusive jet double differential cross-sections were calculated with non-perturbative correction using the CT18NNLO PDFs. It was observed that the theoretical predictions concurred with the experimental data. Thereafter, the correlation $ \mathrm{c}\mathrm{o}\mathrm{s}\phi $ was established between theoretical predictions for the inclusive jet double differential cross-sections and the CT18NNLO gluon PDFs. Finally, the ePump was applied to update the CT18NNLO PDFs; the differences between these data and the original global fitting data were investigated. The CT18NNLO gluon PDFs and ePump updated gluon PDFs were compared at $ Q=100 $ GeV, and it was found that the ATLAS 2.76 TeV inclusive jet double differential cross-sections data could slightly constrain the CT18NNLO gluon PDFs at both small and large $ x $ regions. Figures and Tables | References | Related Articles | Metrics

Select

Research on an isothermal remanent magnetization detection system based on the rubidium atomic ensemble Yue CHEN, Zichang WANG, Guzhi BAO, Yuan WU, Liqing CHEN 2024, 2024 (4):  40-46.  doi: 10.3969/j.issn.1000-5641.2024.04.004 Abstract ( 126 )   HTML ( 3 )   PDF (1036KB) ( 99 )   Save Isothermal remanent magnetization(IRM) is an important research topic in the analysis of material magnetic characteristics. However, owing to its low sensitivity, large volume, and high maintenance cost, the classical IRM measurement system cannot satisfy the practical requirements. Therefore, it is necessary to develop the IRM measurement system to attain a high sensitivity and small size. The magnetic field measurement technology based on the rubidium atomic ensemble has the advantages of high sensitivity and small size; accordingly, in this study, an IRM measurement system based on rubidium atomic ensemble is proposed. Here we focus on the design process regarding the magnetization device and residual magnetism detection device. More importantly, the IRM measurement system can successfully detect the soil samples collected from the Cherry River in Minhang Campus of East China Normal University. Our research demonstrates that the proposed detection system is easy to operate and maintain. Moreover, it has significant application prospects in the fields of environmental magnetism, geological exploration, and biological magnetic field measurement. Figures and Tables | References | Related Articles | Metrics

Select

High-fidelity transmission of optical polarization based on beam splitters Yufei LIN, Wei XIE 2024, 2024 (4):  47-56.  doi: 10.3969/j.issn.1000-5641.2024.04.005 Abstract ( 126 )   HTML ( 4 )   PDF (1169KB) ( 128 )   Save Optical polarization is a fundamental property of light, and it is therefore important to realize the high-fidelity transmission of optical polarization during the optical signal detection process. The optical beam splitter, as a conventional element to build the detection optical path /optical system, could significantly affect the polarization resolution capability of the entire detection system. Based on the theoretical analysis of optical transmission and reflection, polarization-preserving optical pathes with beam splitters can be designed to achieve both reflection and transmission polarization-preserving functions. Experimental data demonstrates that the optical path polarization fidelity is up to 95%. The polarization fidelity design scheme has characteristics including low cost, flexible adjustment and strong functionality, which provides further possibilities for the analysis and application of polarized light. Figures and Tables | References | Related Articles | Metrics

Select

Gas phase formation mechanism of the interstellar molecule 1-cyano-1,3-butadiene Huimin ZHENG, Xilin BAI, Qi’ang GONG, Tao YANG 2024, 2024 (4):  57-64.  doi: 10.3969/j.issn.1000-5641.2024.04.006 Abstract ( 108 )   HTML ( 4 )   PDF (1328KB) ( 97 )   Save In this study, a combination of synchrotron vacuum ultraviolet photoionization experiments and quantum chemical calculations was employed to investigate the reaction mechanism between cyanomethyl radicals (·CH2CN) and propyne (C3H4) in high-temperature interstellar environments. The aim was to gain further insights into the formation mechanism of interstellar organic nitriles. By analyzing the photoionization mass spectra and photoionization efficiency curves, it was determined that the reaction may predominantly yield the open-chain isomers of 1-cyano-1,3-butadiene. Additionally, the reaction potential energy surface was explored at the B3LYP/cc-pVTZ level, revealing a barrierless addition of the cyanomethyl radical to acetylene. This addition mainly leads to the formation of gauche-E-1-cyano-1,3-butadiene and/or E-1-cyano-1,3-butadiene. Conversely, the more thermodynamically stable product, pyridine, exhibits a lower likelihood of formation. Figures and Tables | References | Related Articles | Metrics

Select

Isotope separation method based on nanobubble technology Xuhui ZHU, Banglin CHEN 2024, 2024 (4):  65-70.  doi: 10.3969/j.issn.1000-5641.2024.04.007 Abstract ( 111 )   HTML ( 3 )   PDF (1783KB) ( 52 )   Save This study proposes the nanobubble isotope separation method for the first time. The separation of light elements such as hydrogen, oxygen, carbon, and lithium is realized via experiments, and the separation coefficient is measured, which verifies the scientificity and effectiveness of the method. The study revealed that the isotope separation process of nanobubbles not only occurs when the rapid collapse adiabatic self-shrinkage forms nanobubbles, which causes the dissociation of surface molecules possibly owing to high temperature or nano-surface effects, such that the surface of the bubbles is negatively charged and adsorbs the surrounding medium, but also occurs in the subsequent isotope (ion) chemical exchange process between nanobubbles and specific solutions to form a separation system, which has a dual separation effect. Because the formation of nanobubbles is a rapid process, and the ion exchange between bubbles and solution is an isotopic resonance exchange chemical reaction, the process also quickly reaches equilibrium. The bubbles and solution determine that nanobubble isotope separation is a separation method with a short equilibrium time, overcoming the shortcomings of the usual chemical method balance time. Based on the prototype stand-alone machine for nanobubble separation, nanobubble isotope separation cascades are also designed to increase the separation effect to obtain isotopes of various abundances, thereby illustrating the possibility of industrial production. Figures and Tables | References | Related Articles | Metrics

Life Sciences

Select

Species diversity of bryophytes on Dajinshan Island, Shanghai Ruiping SHI, Peng ZHENG, Qi WU, Yiran WANG, Xiaolu DING, Xuedi GAO, Youfang WANG, Jian WANG 2024, 2024 (4):  71-81.  doi: 10.3969/j.issn.1000-5641.2024.04.008 Abstract ( 124 )   HTML ( 5 )   PDF (734KB) ( 100 )   Save The aim of this study was to update the bryophyte list of Dajinshan Island and provide the scientific basic data for in situ conservation. Based on five field investigations on the island, 67 species belonging to 38 genera in 20 families are reported herein. Compared with historical data for Dajinshan Island, 23 species are newly recorded in the island. Of these, 13 species are newly recorded in Shanghai. One epiphyllous liverwort species, Cololejeunea raduliloba Steph., is newly reported on Dajinshan Island. Taking into account climate change and the physiological and ecological characteristics of bryophytes, the changes in bryophyte species composition on Dajinshan Island are discussed. Our results highlight the importance of timely updating of a regional checklist, when conserving bryophyte biodiversity. Figures and Tables | References | Related Articles | Metrics

Select

Arrangement and analysis of type specimens of the Shanghai Natural History Museum Herbarium Ruiping SHI, Bicheng LI, Chunqing Wen, Yunfei ZHANG, Qianqian WU, Xiangkun QIN 2024, 2024 (4):  82-99.  doi: 10.3969/j.issn.1000-5641.2024.04.009 Abstract ( 125 )   HTML ( 5 )   PDF (13433KB) ( 58 )   Save To ascertain the status and promote the utilization and sharing of type specimens in Herbarium of Shanghai Natural History Museum (SHM), the collecting information of normal specimens in SHM with type specimens in specimens of plant resource sharing platform and journal of plant taxonomy were compared, 418 type specimens were confirmed. There are 239 species belonging to 147 genera in 69 families, including 390 type specimens newly discovered. The quantity, type, species, dominant groups, collectiion location, collection time, and the name type specimen collector were collected and analysed in the herbarium. Figures and Tables | References | Related Articles | Metrics

Select

Bioinformatics-based construction of immune prognostic gene model for hepatocellular carcinoma and preliminary model validation Linding XIE, Yuan ZHANG, Yihong CAI 2024, 2024 (4):  100-110.  doi: 10.3969/j.issn.1000-5641.2024.04.010 Abstract ( 177 )   HTML ( 5 )   PDF (4520KB) ( 51 )   Save The Cancer Genome Atlas (TCGA) and the International Cancer Genome Consortium (ICGC) databases were used to collect RNA sequence information from patients with hepatocellular carcinoma (HCC). The key genes involved in the immune response mechanism to HCC were screened using the non-negative matrix factorization (NMF) clustering method and weighted gene co-expression network analysis (WGCNA). Prognostic gene models were constructed using the least absolute shrinkage and selection operator (LASSO) regression analysis, and biological functions were analyzed using gene set enrichment analysis (GSEA). Subsequently, to assess the immune infiltration and the related functional differences between the patients in two different risk groups , we used single-sample gene set enrichment analysis (ssGSEA). We constructed column line graphs in combination with independent risk factors to predict overall patient survival time using the “RMS” package in R. Finally, preliminary clinical validation was performed using the Human Protein Atlas (HPA) database with real-time quantitative fluorescent PCR (RT-qPCR). In conclusion, we integrated the clinical characteristics of patients based on risk scores to construct a verifiable and reproducible column line chart, providing a reliable reference for the precise treatment of patients in clinical oncology. Figures and Tables | References | Related Articles | Metrics

Select

Effects of 8-week altitude training on the erythropoiesis, iron metabolism, and aerobic capacity in trained rowers Yuxin WANG, Zhirui YU, Tao LI, Shilei LIANG, Huan GAO 2024, 2024 (4):  111-122.  doi: 10.3969/j.issn.1000-5641.2024.04.011 Abstract ( 128 )   HTML ( 5 )   PDF (1232KB) ( 105 )   Save This study was conducted to evaluate the effects of an 8-week altitude training on erythropoiesis, iron metabolism, and aerobic capacity in trained rowers. Twenty-eight trained rowers were divided into the altitude training (AT) and sea-level training (ST) groups. During the 8-week training camp, the training plan and load were similar in both groups. VO2peak, red blood cell count (RBC), reticulocyte% (RET%), hemoglobin (Hgb), and concentrations of serum erythroferrone (ERFE), ferritin (FER), and soluble transferrin receptor (sTfR) were measured before and after the 8-week training camp. It found that (1) compared with the pre-value, VO2peak and VO2peak to body mass (RVO2peak) increased significantly after the 8-week training in the AT group. No obvious differences in VO2peak and RVO2peak were observed in the ST group. The changes in VO2peak and RVO2peak between the two groups were significant (+9.41% vs +3.03%, p<0.05; +12.83% vs +0.80%, p<0.01). (2) After the 8-week training, the RBC, Hgb, and hematocrit (HCT) increased in the AT group but no statistical difference in the ST group. Changes in Hgb and HCT between the two groups were significant (+4.95% vs –3.21%, p<0.01; +6.48% vs –1.57%, p<0.01). A significant trend in RBC count change was observed between the two groups (+3.19% vs –3.61%, p=0.061). Compared with the pre-test values, no significant changes in RET% and reticulocyte hemoglobin equivalent (RET-He) were found in either groups after the 8-week training. The AT group showed significantly increased of low fluorescent reticulocyte (LFR) and reticulocyte production index (RPI) and significantly decreased medium fluorescent reticulocyte (MFR) and high fluorescent reticulocyte (HFR). There were no significant differences in RET%, RET-He, LFR, MFR, HFR, and IRF (immature reticulocyte fraction) in both groups. However, changes in RPI between both groups after the training camp was significant (+30.60% vs –4.52%, p<0.05). (3) In the AT group, no remarkable changes in serum ERFE, a significant decrease in serum FER, and an increase in serum sTfR and sTfR/lg(FER) levels were observed after of the 8-week training. In the ST group, there were no statistical changes in serum FER, sTfR, and sTfR/lg(FER) and significantly increased serum ERFE. Changes in serum FER, ERFE, sTfR, and sTfR/lg(FER) levels differed significantly between both groups (+17.99% vs +121.31%, p<0.05; –36.16% vs –2.96%, p<0.05; +82.77% vs –8.87%, p<0.05; +108.40% vs –6.96%, p<0.05). (4) There was a significantly positive association between the change in VO2peak and serum sTfR levels and ratio of sTfR to lg(FER) after the 8-week training. Therefore , eight weeks of AT appears to be more effective than ST in improving the oxygen delivery capacity of the blood and aerobic capacity in trained rowers. In the later stage of the 8-week AT, erythropoiesis remained active. Serum sTfR levels may be important in improving aerobic performance. Figures and Tables | References | Related Articles | Metrics

Remote Sensing and Geographic Information System

Select

Machine learning-based remote sensing retrievals of dissolved organic carbon in the Yangtze River Estuary Hao CHEN, Xianqiang HE, Run LI, Fang CAO 2024, 2024 (4):  123-136.  doi: 10.3969/j.issn.1000-5641.2024.04.012 Abstract ( 219 )   HTML ( 13 )   PDF (17080KB) ( 82 )   Save Dissolved organic carbon (DOC) is the largest reservoir of active organic matter in the ocean. Accurate characterization of the spatial and temporal patterns of DOC in large-river estuaries and neighboring coastal margins will help improve our understanding of biogeochemical processes and the fate of fluvial DOC across the estuary−coastal ocean continuum. By retrieving the absorption properties of colored dissolved organic matter (CDOM) in the dissolved organic matter (DOM) pool using machine learning models, and based on the correlation between CDOM absorption and DOC concentrations, we developed an ocean DOC algorithm for the GOCI satellite. The results indicated that the Nu-Supporting Vector Regression model performed best in retrieving CDOM absorption properties, with mean absolute percent differences (MAPD) of 32% and 8.6% for the CDOM absorption coefficient at 300 nm (aCDOM(300)) and CDOM spectral slope over the wavelength range of 275 ~ 295 nm (S275–295). Estimates of DOC concentrations based on the seasonal linear relationship between aCDOM(300) and DOC were achieved with high retrieval accuracy, with MAPD of 11% and 14% for the training dataset using field measurements and validation datasets on satellite platforms, respectively. Application of the DOC algorithm to GOCI satellite imagery revealed that DOC levels varied dramatically at both seasonal and hourly scales. Elevated surface DOC concentrations were largely associated with summer and lower DOC concentrations in winter as a result of seasonal cycles of Yangtze River discharges. The DOC also changed rapidly on an hourly scale due to the influence of the tide and local wind regimes. This study provides a useful method to improve our understanding of DOC dynamics and their environmental controls across the estuarine −coastal ocean continuum. Figures and Tables | References | Related Articles | Metrics

Select

Accounting and change analysis of ecological asset in Yingpu Street, Shanghai Chen ZHANG, Zhi TANG, Yan LU, Rui LI, Zhongyang GUO 2024, 2024 (4):  137-149.  doi: 10.3969/j.issn.1000-5641.2024.04.013 Abstract ( 82 )   HTML ( 5 )   PDF (4177KB) ( 45 )   Save This study investigated the ecological assets of Yingpu Street, Shanghai, using historical aerial imagery data. Using various methods, such as the ecological assets balance sheet and correlation analysis, changes in the ecological assets of Yingpu from 2000 to 2021, as well as the underlying mechanisms behind these changes, were analyzed. The results showed that, in 2021, the ecological assets of Yingpu Street mainly consisted of arable land, wetlands, and grasslands with an overall moderate quality. The total ESV(ecological service value) was 9.39 × 106 CNY (Chinese Yuan) and was mainly due to contributions from water conservation and waste treatment services. The ecological assets of Yingpu decreased significantly during the period from 2000 to 2021, with the stock and flow decreasing by 33.07 and 22.97%, respectively. Urban construction led to a reduction in farmland ecological assets and was the major contributor to the overall decline observed. Returning farmlands to forests and grasslands played a key role in the substantial increase of forest and grassland ecological assets. The ESV of Yingpu was negatively correlated with night light intensity, population, GDP (gross domestic product), land surface temperature, and DEM (digital elevation model) (p < 0.001), but was positively correlated with slope (p < 0.001). Figures and Tables | References | Related Articles | Metrics

Estuary and Coastal Research

Select

Research on the impact of a typhoon on the accretion-erosion of mudflats: Based on UAV photogrammetry and in situ hydrodynamic measurements Xinmiao ZHANG, Liming XUE, Benwei SHI, Wenxiang ZHANG, Tianyou LI, Biaobiao PENG, Xiuzhen LI, Yaping WANG 2024, 2024 (4):  150-160.  doi: 10.3969/j.issn.1000-5641.2024.04.014 Abstract ( 143 )   HTML ( 10 )   PDF (2685KB) ( 182 )   Save Extreme events such as typhoons can change mudflats by tens of centimeters. It is important for coastal management and ecosystem maintenance to recognize changes in accretion-erosion during typhoons and to understand the mechanisms driving it. In this study, Unmanned Aerial Vehicle (UAV) photogrammetry based on the Structure-from-Motion (SfM) algorithm was used to generate Digital Elevation Models (DEM) of a mudflat in Eastern Chongming, Yangtze Estuary, before and after the passage of Typhoon “In-Fa” (July 2021). Hydrodynamic measurements were conducted from bare flats to marshes to explore the mechanisms of DEM changes. Changes in accretion-erosion observed by UAV photogrammetry presented an obvious zonation of eroded bare flats and accreted marshes. The accuracy of the DEMs is 4.1 cm. Under the impact of the typhoon, the erosion of the bare flat and the accretion of the marsh have a amplitude of ±32 cm. During typhoons, the wave height and water depth in the bare flat increases to the condition of wave breaking, and the surface sediment is eroded and carried by rising tides. But in marshes, the sediment carrying capacity of water columns decreases, and the sediments are deposited. Consequently, the mudflat presents an obvious zonation of accretion-erosion. This study provides a new perspective for deeply understanding the impact of typhoons on the accretion-erosion of mudflats by combining UAV photogrammetry and hydrodynamic measurements. Figures and Tables | References | Related Articles | Metrics