华东师范大学学报（自然科学版）

Select

一种面向嵌入式操作系统的形式化验证方法

王阳, 方竟成, 蔡雄, 张志鹏, 蔡喁, 缪炜恺

2024 (4): 1-17. doi: 10.3969/j.issn.1000-5641.2024.04.001

摘要 ( 216 )

HTML ( 13 )

PDF(1364KB) ( 255 )

操作系统是整个计算机系统的核心与基石, 其可靠性与安全性至关重要. 操作系统的故障或漏洞可能会导致系统崩溃、数据丢失、隐私泄露和安全攻击等问题, 特别是在安全攸关系统中, 一旦操作系统发生错误, 就可能会造成重大人员伤亡或财产损失. 一直以来, 如何保障操作系统的安全性和可靠性对学术界和工业界都是一个重大挑战. 目前验证操作系统安全性的方法有软件测试、程序静态分析、形式化方法等. 其中, 形式化方法是最有潜力确保操作系统安全可信的方法, 通过使用形式化方法, 建立数学模型并进行系统的形式化分析和验证, 从而发现潜在的错误和漏洞. 在操作系统中, 形式化方法可以用于验证操作系统的功能正确性、完整性以及系统安全性等. 在已有的针对操作系统形式化验证的成果基础上, 提出了一个面向嵌入式操作系统的形式化验证方案, 采用VCC (verified C compiler)、CBMC (C bounded model checker)以及PAT (process analysis toolkit)工具分别对操作系统单元层面、模块层面和系统层面进行验证. 该方法已成功应用到某操作系统的任务调度架构案例中, 对于嵌入式操作系统的分析验证具有一定的通用性.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

一种基于机器学习的模型检查算法性能预测方法

张枨宇, 诸嘉逸, 黄怿豪, 杨迪, 李建文, 缪炜恺, 阎迪, 顾斌, 詹乃军, 蒲戈光

2024 (4): 18-29. doi: 10.3969/j.issn.1000-5641.2024.04.002

摘要 ( 127 )

HTML ( 10 )

PDF(2393KB) ( 102 )

与非图模型是一种表示电路设计的通用基础形式, 同时也是模型检查器的一种通用输入格式. 介绍了一种基于与非图结构编码的特征提取方法, 并基于该方法实现了一种快速的组合模型检查器Liquid. 所提出的结构编码的核心思想: 首先罗列出与非图中所有可能的子结构, 再将每个子结构出现的次数编码成向量, 该向量即作为与非图的特征向量参与之后的机器学习过程. 由于各种模型检查算法的性能在不同的与非图上参差不齐, Liquid的设计目标是组合多种模型检查算法, 针对不同的与非图使用机器学习模型挑选出合适的算法. 收集了目前所有的模型检查器基准测试集作为实验数据集并进行了实验. 实验结果表明, Liquid在实验数据集上的表现优于所有组合中的独立模型检查算法, 并有着不错的预测准确率. 同时, 还从多个维度分析了Liquid有效的原因.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

ATLAS 2.76 TeV单喷注实验数据对CT18NNLO部分子分布函数的影响

徐颖, 范红豪, 沙依甫加马力·达吾来提

2024 (4): 30-39. doi: 10.3969/j.issn.1000-5641.2024.04.003

摘要 ( 74 )

HTML ( 5 )

PDF(1182KB) ( 31 )

通过ePump (error PDF (parton distribution function) updating method package)研究了大型强子对撞机(large hadron collider, LHC)在质心能量$ \sqrt{s}=2.76 $ TeV时, 来自ATLAS (a toroidal LHC apparatus)探测器单喷注的双微分散射截面的实验数据对CT18NNLO (next-to-next-to-leading order)部分子分布函数(PDF)的影响. 首先, 使用CT18NNLO 部分子分布函数计算了单喷注的双微分散射截面, 观察到理论预测与实验数据符合得较好; 其次, 计算了单喷注双微分散射截面的理论预测值与CT18NNLO胶子部分子分布函数的关联余弦$\mathrm{c}\mathrm{o}\mathrm{s}\phi$; 最后, 使用ePump更新了CT18NNLO 部分子分布函数, 并研究了实验数据与全局拟合数据间的冲突. 通过比较在$ Q=100 $ GeV时CT18NNLO 胶子部分子分布函数和ePump更新的胶子部分子分布函数, 发现ATLAS 2.76 TeV单喷注双微分散射截面实验数据在大和小的动量分数$ x $区域对CT18NNLO 胶子部分子分布函数的约束较小.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

基于铷原子系综的等温剩磁检测系统研究

陈悦, 王梓畅, 包谷之, 吴媛, 陈丽清

2024 (4): 40-46. doi: 10.3969/j.issn.1000-5641.2024.04.004

摘要 ( 126 )

HTML ( 3 )

PDF(1036KB) ( 99 )

等温剩磁(isothermal remanent magnetization, IRM)是物质磁性测量分析的重要研究内容之一. 然而, 常用的等温剩磁测量系统因测量灵敏度低、体积庞大且维护成本高等问题无法满足实际使用要求. 因此, 设计并研制测量精度高且便于使用的小型化等温剩磁检测系统成为必然, 其中, 基于铷原子系综的磁场测量技术具有灵敏度高、易小型化等优点. 利用该磁场检测技术, 设计并搭建了等温剩磁检测系统, 着重介绍了磁化装置、剩磁检测装置等核心部件的设计方案, 并成功地对采自华东师范大学闵行校区樱桃河附近表层土壤进行了检测, 实现了该土壤等温剩磁曲线的测量. 研究表明, 该系统操作容易且便于维护, 在环境磁学、地质勘探和生物磁场测量领域有很重要的应用前景.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

基于分束器的光学偏振保真传输

林雨菲, 谢微

2024 (4): 47-56. doi: 10.3969/j.issn.1000-5641.2024.04.005

摘要 ( 126 )

HTML ( 4 )

PDF(1169KB) ( 128 )

光的偏振作为光的基本禀性之一, 在光信号获取分析应用中至关重要. 光学分束器作为搭建探测光路/光学系统的常规元件, 其对光偏振信息的保真传输效果会极大地影响整个探测系统的偏振检测能力. 通过光学透反射理论分析, 基于光学分束器设计出了同时满足反射保偏和透射保偏功能的光路. 实验证明该光路的偏振保真度高达95%以上. 此光路设计方案具有成本低、调节灵活、功能性强等特点, 为偏振光的分析和应用提供了更多的可能性.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

星际分子1-氰基-1,3-丁二烯的气相合成机制研究

郑慧敏, 白西林, 龚起昂, 杨涛

2024 (4): 57-64. doi: 10.3969/j.issn.1000-5641.2024.04.006

摘要 ( 108 )

HTML ( 4 )

PDF(1328KB) ( 97 )

为深入了解星际有机腈分子的动力学生成机制, 结合同步辐射真空紫外光电离实验和量子化学计算, 研究了高温星际环境中氰甲基自由基 (·CH₂CN) 与丙炔 (C₃H₄) 的反应机制. 通过分析光电离质谱与光电离效率图, 发现反应可能主要产生1-氰基-1,3-丁二烯开链异构体. 继而, 在B3LYP/cc-pVTZ水平上计算了反应势能面, 发现氰甲基自由基可无势垒地加成到丙炔上, 主要产生gauche-E-1-氰基-1,3-丁二烯和E-1-氰基-1,3-丁二烯这两种产物, 而热力学上更稳定的产物吡啶的生成概率较小.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

纳米气泡分离同位素方法初研

诸旭辉, 陈邦林

2024 (4): 65-70. doi: 10.3969/j.issn.1000-5641.2024.04.007

摘要 ( 111 )

HTML ( 3 )

PDF(1783KB) ( 52 )

首次了提出纳米气泡同位素分离方法, 并通过实验实现了氢、氧、碳和锂等轻同位素的分离, 测得了分离系数, 验证了该方法的科学性和有效性. 研究揭示了纳米气泡同位素分离过程首先发生在由于快速塌陷式绝热自收缩形成纳米气泡时,可能因高温或纳米表面效应作用引起表面分子离解, 而使气泡表面带负电荷对周围介质的吸附过程中, 并且也出现在后续纳米气泡与特定溶液组成分离体系的同位素 (离子) 化学交换过程中, 它具有双重分离效应. 由于纳米气泡的形成是一个快速过程, 并且气泡在溶液中的离子交换是同位素共振交换化学反应, 过程也很快达到平衡, 两者共同决定了纳米气泡同位素分离可能是一种平衡时间很短的分离方法, 克服了通常化学方法平衡时间长的缺点. 在研制成纳米气泡分离原型单机的基础上, 本文也设计了纳米气泡同位素分离级联, 增加分离效果, 以获得各种丰度的同位素, 从而说明其工业化生产的可能性.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

上海大金山岛苔藓植物物种多样性

师瑞萍, 郑鹏, 吴琪, 王怡然, 丁晓璐, 高雪笛, 王幼芳, 王健

2024 (4): 71-81. doi: 10.3969/j.issn.1000-5641.2024.04.008

摘要 ( 124 )

HTML ( 5 )

PDF(734KB) ( 100 )

为了及时更新大金山岛苔藓植物名录, 为其就地保护研究提供科学依据, 在对上海大金山岛5次野外调查的基础上, 报道了大金山岛苔藓植物20科38属67种, 与该岛历史数据相比, 新增23种苔藓植物, 包括上海新记录13种, 首次发现叶附生苔类植物 (拟疣鳞苔Cololejeunea raduliloba Steph.) 在大金山岛的分布. 结合气候变化及苔藓植物生理生态特性对大金山岛苔藓植物物种组成变化进行了讨论, 提出了及时更新一个地区的名录对多样性就地保护的重要性.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

上海自然博物馆植物标本室模式标本的整理与分析

师瑞萍, 李必成, 文春青, 张云飞, 吴倩倩, 秦祥堃

2024 (4): 82-99. doi: 10.3969/j.issn.1000-5641.2024.04.009

摘要 ( 125 )

HTML ( 5 )

PDF(13433KB) ( 58 )

为进一步厘清上海自然博物馆植物标本室模式标本的基本情况, 促进标本的利用和共享, 通过比对馆藏标本与植物标本资源共享平台和植物分类学期刊中模式标本的采集信息, 整理出模式标本418份, 隶属69科147属239种, 其中新发现模式标本390份. 本文还对馆藏模式标本的数量、类型、种类组成、优势类群、采集地、采集时间及采集人等进行了统计和分析.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

基于生物信息学构建肝癌免疫预后基因模型及初步验证

谢琳玎, 张远, 蔡亦红

2024 (4): 100-110. doi: 10.3969/j.issn.1000-5641.2024.04.010

摘要 ( 177 )

HTML ( 5 )

PDF(4520KB) ( 51 )

利用癌症基因组图谱 (the Cancer Genome Atlas, TCGA) 和国际肿瘤基因组协作组 (International Cancer Genome Consortium, ICGC) 数据库收集肝细胞癌 (hepatocellular carcinoma, HCC) 患者的RNA测序信息. 首先, 通过非负矩阵分解 (non-negative matrix factorization, NMF) 聚类方法和加权基因共表达网络分析 (weighted gene co-expression network analysis, WGCNA) 筛选出参与HCC免疫反应机制的关键基因. 利用套索 (the least absolute shrinkage and selection operator, LASSO) 回归分析构建预后基因模型, 并用基因集富集分析 (gene set enrichment analysis, GSEA) 方法分析生物学功能. 随后, 对不同风险组患者使用单样本基因集富集分析 (single sample genes set enrichment analysis, ssGSEA) 评估两组间免疫浸润和相关功能差异. 使用 “RMS” R软件包结合独立危险因素构建列线图以预测患者的总体生存时间. 最后, 利用人类蛋白质图谱数据库(Human Protein Atlas, HPA)与实时荧光定量PCR (real-time quantitative PCR, RT-qPCR) 进行临床初步验证. 总之, 本文在风险评分的基础上整合患者临床特征, 构建了一个可验证、可重复的列线图, 为临床肿瘤患者的精准治疗提供可靠的参考.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

8周高原训练对赛艇运动员红细胞生成、铁代谢和有氧运动能力的影响

王玉新, 余知睿, 李涛, 梁世雷, 高欢

2024 (4): 111-122. doi: 10.3969/j.issn.1000-5641.2024.04.011

摘要 ( 128 )

HTML ( 5 )

PDF(1232KB) ( 105 )

以28名男子赛艇运动员作为研究对象, 分为高原组和平原组, 旨在探讨持续8周的高原训练对男子赛艇运动员红细胞生成、铁代谢和有氧运动能力的影响. 8周训练期间两组运动员均执行相同的训练计划, 训练负荷基本保持一致. 分别测量8周训练前后的最大摄氧量(VO_2peak)和循环血红细胞计数(RBC)、网织红细胞(RET)%、血红蛋白(Hgb)浓度等红细胞参数, 以及红铁酮(ERFE)、铁蛋白(FER)、可溶性转铁蛋白受体(sTfR)水平. 研究结果发现: ① 与训练前相比, 8周训练后高原组的VO_2peak、RVO_2peak(相对体重最大摄氧量)显著升高, 平原组均无显著变化, 两组间VO_2peak、RVO_2peak的变化均存在显著差异 (+9.41% vs +3.03%, p<0.05; +12.83% vs +0.80%, p<0.01). ② 8周训练后, 高原组的RBC、Hgb、HCT (红细胞压积)均显著升高, 平原组略微下降. 两组间Hgb、HCT的变化存在显著差异 (+4.95% vs –3.21%, p<0.01; +6.48% vs –1.57%, p<0.01), RBC存在显著差异的趋势 (+3.19% vs –3.61%, p=0.061); 高原组和平原组的RET%、RET-He (网织红细胞血红蛋白含量)均未发生显著改变; 但高原组的LFR (低荧光强度网织红细胞)、RPI (网织红细胞生成指数)显著升高, MFR (中荧光强度网织红细胞)、IRF (幼稚网织红细胞比率)均显著下降; 两组间RPI的变化存在显著差异 (+30.60% vs –4.52%, p<0.05). ③ 8周训练后, 高原组的FER显著下降, sTfR、sTfR/lg(FER)显著升高, ERFE无显著变化; 平原组的ERFE显著升高, FER、sTfR、sTfR/lg(FER)均未发生显著改变; 两组间FER、ERFE、sTfR、sTfR/lg(FER)的变化存在显著差异 (+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). ④ 8周训练后, VO_2peak的变化幅度仅与循环血sTfR、sTfR/lg(FER) 的变化幅度呈显著正相关. 由此得出结论: 持续8周的高原训练有助于提高赛艇运动员有氧运动能力和循环血的氧转运能力. 8周高原训练后期, 红细胞生物合成依然较为活跃. sTfR在有氧能力的改善中可能发挥着重要作用.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

基于机器学习的长江口表层水体溶解有机碳遥感反演研究

陈灏, 何贤强, 李润, 曹芳

2024 (4): 123-136. doi: 10.3969/j.issn.1000-5641.2024.04.012

摘要 ( 219 )

HTML ( 13 )

PDF(17080KB) ( 82 )

溶解有机碳 (dissolved organic carbon, DOC) 是海洋中最大的活跃有机碳库. 精确刻画大河河口及其近海水体表层DOC浓度的时空分布, 有助于更好地理解河流输送的有机碳在河口近海经历的生物地化过程及在该区域的归宿. 本研究采用机器学习方法, 通过反演水体溶解态有机碳库中的有色溶解有机物 (colored dissolved organic matter, CDOM) 的吸收光谱信息, 并基于其与水体DOC浓度的相关关系, 发展了基于地球静止轨道水色成像仪 (geostationary ocean color imager, GOCI) 的DOC遥感反演模型. 结果表明, Nu支持向量回归 (nu-supporting vector regression, NuSVR) 方法可准确反演CDOM光谱吸收特性 (如验证集CDOM在300 nm处的吸收系数a_CDOM(300)和275 ~ 295 nm处的光谱斜率S_275–295的平均绝对误差 (mean absolute percent differences, MAPD) 分别为32%和8.6%). 分别基于该区域表层水体CDOM光谱吸收特性与DOC浓度之间表现的3种不同的相关关系进行DOC算法构建, 结果表明, 基于a_CDOM(300)与DOC浓度之间的线性相关, 并考虑这一相关关系的季节性差异所构建的DOC反演算法可较为准确地反演水体DOC浓度, DOC反演现场数据验证集和卫星验证集的MAPD分别为11%和14%. 将构建的DOC算法模型应用到GOCI卫星图像上, 结果显示, 受长江径流影响, 季节尺度上, 长江口夏季水体表层DOC浓度显著高于冬季; 而受潮汐、风场等因素的影响, 小时尺度上河口近岸海域DOC分布呈现逐时高动态变化. 本研究利用卫星遥感反演河口近海水体DOC浓度, 为进一步在不同时间尺度上研究该区域水体DOC动态变化及驱动因素提供了有效手段.

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

上海市盈浦街道生态资产核算与变化分析

张谌, 汤志, 陆衍, 李蕊, 过仲阳

2024 (4): 137-149. doi: 10.3969/j.issn.1000-5641.2024.04.013

摘要 ( 82 )

HTML ( 5 )

PDF(4177KB) ( 45 )

以上海市青浦区盈浦街道为例, 基于历史航空影像数据对区域生态资产进行调查, 通过生态资产损益表和相关分析等方法研究了2000—2021年盈浦街道生态资产变化趋势及原因. 结果表明: 2021年盈浦街道生态资产存量以耕地、湿地和草地为主, 质量等级总体为中级; 流量总价值为9.39 × 10⁶元, 以水源涵养和废物处理价值为主. 2000—2021年期间, 盈浦街道生态资产总量呈显著下降趋势, 存量和流量分别下降了33.07%和22.97%. 城镇建设导致耕地生态资产迅速缩减是盈浦街道生态资产存量下降的主要因素, 退耕还林和退耕还草是盈浦街道林地和草地生态资产大幅增加的关键原因. 盈浦街道生态资产流量价值与夜间灯光强度、人口数量、国内生产总值、地表温度和高程呈负相关关系 (p < 0.001), 与坡度呈正相关关系 (p < 0.001).

数据和表 | 参考文献 | 相关文章 | 计量指标

Select

台风对淤泥质潮滩冲淤影响研究——基于无人机测量与现场水动力观测

张新淼, 薛力铭, 史本伟, 张文祥, 李天佑, 彭彪彪, 李秀珍, 汪亚平

2024 (4): 150-160. doi: 10.3969/j.issn.1000-5641.2024.04.014

摘要 ( 143 )

HTML ( 10 )

PDF(2685KB) ( 182 )

台风等极端天气会使淤泥质潮滩发生数十厘米的冲淤变化. 在全球变暖导致台风强度及频率增大的背景下, 厘清台风影响下潮滩冲淤变化及其机制, 对潮滩保护与生态系统完整性维持具有重要意义. 本文借助基于运动恢复结构算法的无人机(unmanned aerial vehicle, UAV)摄影测量方法, 于2021年7月“烟花”台风前后对崇明东滩典型样地进行滩面高程测量, 并在盐沼-光滩过渡带现场采集水动力泥沙数据. 结果表明: 无人机摄影测量精度为4.1 cm; 台风影响下光滩区域侵蚀、盐沼区域淤积, 变幅达 ±32 cm. 其原因是: 台风影响下, 光滩区域在天文大潮时波高及水深增大, 达到波浪破碎条件后表层沉积物被侵蚀并被强潮流搬运; 涨潮流携带悬浮泥沙进入盐沼后, 因盐沼缓流消浪作用导致水体挟沙能力下降, 泥沙在盐沼区域沉积. 因此, 盐沼-光滩过渡带呈现光滩区域侵蚀、盐沼区域沉积的冲淤分带性. 本文将无人机摄影测量与同步水动力泥沙现场观测结合, 为深刻认识台风事件对潮滩冲淤的影响提供了新视角.

数据和表 | 参考文献 | 相关文章 | 计量指标

当期目录