教学课程资源库 更多>>

关键词： 形式化验证   错误传播   测试需求   测试用例   网构件  

摘要： 随着科技飞速发展,人们可以在越来越多的领域里发现计算机的身影。计算机带来便捷的同时,同样也会带来一些不可忽略的安全问题。计算机系统运行时发生的故障或者产生的漏洞可能会被某些黑客利用,对用户的电脑进行攻击,给用户带来危及生命、财产的重大损失,造成严重危害。存在于构件系统中可能会造成危害的安全漏洞已经成为了不可忽视的问题,因此如何检测构件系统运行时出现的安全问题已经成了软件测试中的热门研究课题。形式化方法是一种依靠数学手段验证或论证来保证软件开发安全的方法,开发人员根据构件的说明文件构建构件自身安全规约并为其建立抽象模型从而分析其中存在的安全隐患。因此本文选择基于形式化的跨主体网构件漏洞检测方法作为研究课题。本文首先提出一种基于形式化的跨主体网构件漏洞检测框架,考虑构件间错误传播情况,构建形式化模型,在此基础上,按照转换规则获得Nu Smv(New Symbolic Model)模型,结合这两种模型对构件逻辑以及功能的进行测试。在此之后,深入研究测试用例生成方法,通过对测试需求的分析构建测试需求模型,并通过模型生成用例需要的标记迁移系统,最终形成一套符合软件测试工作需求的用例生成方法。同时,以本文的研究为基础,设计并实现了基于形式化的跨主体网构件漏洞检测原型系统。本文的主要工作如下:1、提出了基于形式化的跨主体网构件漏洞检测框架,在此框架中,首先选择了单子作为抽象计算的媒介,并且根据构件运行时的调用情况,使用形式化描述语言构建出构件运行过程中产生错误后的错误传播模型。接着分析了构件运行时产生的错误种类,将其分为了显式漏洞以及隐式漏洞,并且分别设计检测算法。然后,深入研究形式化语言与Nu Smv语言之间的语法语义,根据转换规则,通过4个方面的转换,设计了一种将形式化模型转换至Nu Smv模型的转换方法,对系统的功能上可能存在的安全漏洞进行进一步测试。提出的方法也通过实验证明可以较好地检测出构件漏洞。2、提出了一种基于测试需求模型的测试用例生成方法,首先选取被测系统的特征,并且量化这些特征,给出测试特征模型视图。然后选择被待测系统的测试目标并对其进行划分,分组完成后,以某个具体测试目标为对象对其节约束标注,并给出测试目标分组及描述模型视图。接着选取测试目标节点,具体分析后生成测试目标描述模型视图。最后筛选出测试需求关注的构件,并给出基于被测系统构件的测试需求描述模型视图。在获取了上述四个模型视图之后,可以构建出测试需求元模型。通过工具给出被测系统的状态图合集,并根据算法将被测系统状态图合集转化为被测系统的标记迁移系统,随后将测试目标描述模型转化测试目标的标记迁移系统,再通过标记迁移系统生成测试用例。最终通过实验证明本文提出的方法可以优化迁移路径,生成较少的测试用例。3、设计并实现了基于形式化的跨主体网构件漏洞检测原型系统。该原型系统的具体模块为:组件分析模块、形式化验证与测试模块、测试需求建模模块和测试用例生成模块。同时该系统贯穿人性化设计思想,便于操作。

关键词： 锂金属负极   锂枝晶   结构化设计   静电纺丝   金属掺杂   多孔碳纳米纤维  

摘要： 随着现代电子产品、新能源汽车以及大型储能系统的日益发展,人们对二次电池的能量密度和循环寿命提出更高的要求。锂离子电池经过了三十多年的发展,几乎达到了性能瓶颈,无法满足高储能需求的飙升。锂金属负极拥有较低的密度(0.534 g cm)、最低的电化学电势(-3.04 V,相对于标准氢电极)以及超高的理论比容量(3860 mAh g)而备受关注,长期以来被认为是下一代锂电池电极材料中的“圣杯”。然而,一些严峻的挑战严重阻碍了锂金属电池的商业化应用,例如锂枝晶的生长、固有的体积膨胀以及低库伦效率。为了解决锂金属电池存在的上述问题,研究人员已经开拓了多种策略来稳定锂金属负极,包括人工SEI膜的开发、电解质组成优化、锂金属负极的结构化设计。其中,锂金属负极的结构化设计是一种解决锂枝晶生长和体积膨胀问题的有效策略。因此,本文从锂金属负极的结构化设计出发,采用简便的静电纺丝技术以及高温热处理制备了三种不同的金属掺杂多孔碳纳米结构,主要研究工作如下:(1)以乙酰丙酮铁(Fe(CHO))、聚丙烯腈(PAN)、聚甲基丙烯酸甲酯(PMMA)为原料,设计了由铁纳米颗粒装饰的多孔碳纳米纤维(PCNF-Fe)支架,且不需要危险的气氛、昂贵的催化剂沉积、额外的碳源。值得注意的是,获得的PCNF-Fe可以作为锂金属负极主体,在各种电流密度下具有较低的锂沉积过电位以及长循环稳定性。其中,该主体在3 mA cm的电流密度下可以稳定循环220圈,其过电压仅为23 m V左右。多孔的主体结构可以适应锂电镀/剥离过程中固有的体积膨胀以及锂离子的传输,从而提高循环稳定性。密度泛函理论(DFT)计算表明,Fe纳米颗粒修饰的碳纳米纤维更容易吸收锂原子,从而实现更均匀的锂沉积。(2)以四水合乙酸镍(NiCHO·4HO)、PAN、PMMA为原料,设计了由镍纳米颗粒装饰的多孔碳纳米纤维(PCNF-Ni)支架。镍纳米颗粒装饰的N掺杂碳纤维可以暴露更多的活性位点来捕捉锂离子,从而改善其亲锂性。此外,3D多孔的导电结构可以减轻体积膨胀变化,并且可以有效降低局部电流密度以抑制锂枝晶的形成与产生。因此,PCNF-Ni主体展现出了优异的电化学性能。DFT计算结果表明,镍纳米颗粒装饰的碳纳米纤维对锂的吸附能力更强,从而实现更均匀的电镀。(3)以Fe(CHO)、NiCHO·4HO、PAN以及PMMA为原料,设计了由FeNi合金纳米颗粒装饰的多孔碳纳米纤维(PCNF-FeNi)支架。多孔的结构以及FeNi合金的掺入可以暴露更多的锂成核活性位点,有效降低锂金属的成核过电位,以引导锂的均匀沉积。3D结构化的多孔主体可以提供丰富的导电网络以及更大的比表面积,可以缓冲循环过程中的固有体积膨胀并有效降低局部电流密度,调节锂金属的生长而不存在枝晶问题。该主体在3 mA cm的电流密度下可以实现超过220次的稳定循环,并保持较低的过电压。在1 mA cm的电流密度和1 mAh cm的沉积容量下,PCNF-FeNi电极经过300圈循环后库伦效率仍维持在97%左右。本文为设计3D结构化的高效锂金属负极主体提供了低成本且可扩展的策略,同时也为其他金属负极的灵活设计提供了一定的参考。

关键词： 结构化产品   学生群体理财   黄金挂钩结构化存款  

摘要： 截至2020年,中国各类高等教育在学总规模达到4183万人1,高等院校学生群体月人均收入中位数1516元高于国民人均月可支配收入1470元2,正逐步成为中国的主流消费群体,也是未来中国经济增长的核心动力。目前,新时代青年学生群体在一定程度上已具备了一定的资产配置能力与相关的投资理财观念,但非商科学生接受金融相关培训较少,市场中也缺乏适合大学生群体投资理财的途径,因此开发一款针对学生群体的理财产品既可以培养青年学生群体投资意识和能力,也有利于金融机构拓展客户。本文分析了结构化产品定义、市场发展及政策,从银行（发行方）和大学生（投资方）需求出发,提出产品相关参数、挂钩标的、收益模型及营销手段等全流程的设计方案。在产品设计中,本文根据蒙特卡洛模拟和B-S模型对产品进行定价分析;根据Var模型和历史数据对产品进行风险分析;将产品与其他同类产品进行比较分析,并得出以下结论:（1）在目前监管趋严、利率下行的背景下,结构化产品在获得超额的收益同时,风险有限,未来发展潜力大;（2）对于银行来说,产品定价处于合理的水平;对于投资者而言本产品不存在损失本金的可能且仅有11.85%的可能获得低于定期存款的收益率,产品定价、收益和风险符合产品设计初衷;（3）通过与其他产品对比,本产品具有低门槛低风险的优势。因此,本产品的设计具有如下特点:明确产品是“为了吸引学生群体的低风险入门级银行理财”的定位,以拓展客户群体为最终目的,后续将以线下线上相结合的方式开展营销活动。本文对结构化产品及产品市场的详细分析,可以帮助投资者在大监管背景下进一步了解理财产品市场、选择与自身风险偏好相契合的理财产品。本文的产品设计,不仅能帮助学生群体树立正确的投资理念,提供低门槛、稳健的理财产品,而且能提高银行自身揽储能力,为金融机构在大监管背景下进行金融创新、扩展客户提供思路。

关键词： 软件定义   形式化方法   高层次综合   EDA   硬件结构优化  

摘要： 时至今日,信息产业升级对快速芯片设计提出了新的要求。EDA领域尤为重要,同时也是被国家认定的卡脖子的工业软件领域之一。EDA中的高层次综合工具是作为新一代的芯片前端设计工具得到人们追捧,它可以帮助软件开发人员快速通过高级语言实现硬件电路的设计。人们认为软件定义硬件（SDH）的方向是未来EDA工具智能化的重要发展趋势,本研究针对软件定义硬件的高层次综合方法在核心框架、关键算法、工具设计等做出了主要的工作及贡献:1)提出了一种软件定义硬件的高层次综合新方法框架-FastHLS,设计了从二进制指令代码到结构、结构再到系统级电路逐步构造的完整处理过程,即建构过程及其完整工具链。整个处理过程的核心思想是通过降维,将高层次综合问题转化为二进制指令代码翻译的结构与建构的问题,通过设计新算法在结构的维度上寻找满足资源、性能约束条件需求的同构结构,构造这种结构后将其转化为各种硬件体系架构（例如:专用的同步时序逻辑电路、RISC处理器、VLIW架构的处理器结构等）,最终映射到一种抽象的HAC硬件结构完成软件定义硬件的设计,实现了不依赖高级语言编译器下完成SoC级的高层次综合工作,有效地解决了软件开发和硬件自动化设计耦合关系。2)提出了FastHLS核心算法和关键技术的实现细节,其中包括结构优化方法、架构生成方法、特殊结构翻译、调试策略与机制、动态冗余剔除方法等。为了快速实现电路的建构,设计了一种Hrtl（Ib,ω）建构算子,并给出了实现方法和过程,通过反复迭代指令模板完成指令级到模块级的结构构造;为了能够进一步使结构同构满足性能和资源需求,设计了两种结构优化算法:一种是基于最小资源建构约束下尽可能提升性能的MinR-PI优化算法;另一种是优先结构全翻译在并行性及性能优先前提下进行资源约束的BalR-PI优化算法。通过这两个算法可以为开发人员提供更多的硬件结构方案;为了让高层次综合工具达到更好的兼容软件开发及代码可重用目的,设计了RCB-Detect静态分析算法用于检测代码中重复指令序列,并给出可重用模块的组合方案和模块引用建议;为了解决特殊结构、冗余剔除及代码调试上的相关问题,设计了一些特殊指令结构的翻译,例如中断处理、存储器的访问等,设计了在结构上完成动态冗余剔除的算法,可以榨出更多的硬件资源。3)完成了FastHLS工具的开发和评估,对整个工具链进行了实验测试。实验测试结果中发现无论在编译速度、可综合性、芯片资源占用情况等都取得了比同类工具更好的结果。最终,本研究使得高层次综合在可重用性、可靠性、易用性、应用性得到了突破。

关键词： 结构化CBN砂轮   激光3D打印   流场仿真   磨削实验  

摘要： 由于科学技术的高速发展,难加工的硬脆材料、塑性难加工材料依靠其拥有的高强度、高硬度和优良的耐磨性等优势在国防、电子和能源等领域得到广泛应用。普通的磨削已经很难达到需要的工艺技术要求。对于难加工材料,可采用能够实现高速磨削的金刚石砂轮、CBN砂轮。而CBN磨料硬度高、耐高温性能好、化学惰性好,在加工黑金属时比金刚石更合适。砂轮结构化能够有效缓解传统砂轮磨削力大,磨削温度高,砂轮表面堵塞及磨削烧伤等问题。激光3D打印技术利用其根据三维模型数据可以快速精准成型任意复杂结构的特点,若应用于结构化CBN砂轮的制备,则打破传统砂轮的制备局限,实现灵活、精准、绿色的方法制备砂轮。因此本课题研究对新型磨具制备有着很大的实际研究意义和可实践性。论文的主要研究内容包括: (1)砂轮制备工艺与工艺参数的确定。对实验设备进行选择,组成激光3D打印系统。选择相应的磨削设备和检测设备。选择合适的金属复合粉材、CBN磨粒和基体材料作为砂轮制备材料。对影响砂轮成型质量的重要因素进行单因素实验,再进行正交实验和极差分析选择出激光3D打印砂轮最合适的制备工艺参数。 (2)结构化砂轮设计与磨削液流场仿真。对结构化砂轮的结构进行创新与优化,设计三种激光3D打印的结构化砂轮的结构,并设计直线型对照结构,以验证所设计结构化砂轮的可行性与优势。磨削区冷却液流场仿真,对所设计的结构化砂轮进行磨削时冷却液流动压力、湍流动能等进行仿真与分析,为后期的磨削实验结果分析提供一定的理论支持。 (3)结构化砂轮的制备与显微观察。利用相应软件导出程序再输入到3D打印系统中,完成复合粉材与基体材料的前期处理与准备,用确定好的工艺参数进行3D打印砂轮。得到的成型砂轮使用激光共聚焦显微镜进行扫描检测,观察砂轮表面微观状态以及表面CBN磨粒的分布。 (4)砂轮磨削实验与磨削性能分析。利用相应磨削设备对成型的结构化砂轮进行磨削实验,比较不同的磨粒排布结构化砂轮的磨削性能。对工件进行观察与粗糙度测量,对比分析不同结构化砂轮,进行磨削性能评价。圆弧正弦相结合的结构化砂轮磨削得到的工件表面质量最好。

关键词： 结构化理财产品   上证50ETF   双重障碍期权   BSM定价模型   蒙特卡洛模拟  

摘要： 结构化理财产品出现于19世纪50年代,于21世纪初期进入我国金融市场。现阶段我国结构性金融产品的市场体系已初具规模,结构化理财产品在金融市场上发挥的作用也愈发凸显,然而产品定价不合理以及同质化等问题仍然突出。为了能够丰富结构化理财产品种类,为不同的结构化产品提供适用的定价方法,本文为投资者设计出了一款挂钩上证50ETF指数表现的结构化产品,该产品内嵌双重障碍期权,收益结构新颖,降低了风险损失的可能性,提供了较高的潜在收益,为创新金融市场结构化理财产品种类、嵌入双重障碍期权的结构化产品定价提供了新的研究思路,兼具理论意义与实践意义。首先,本文梳理了结构化理财产品以及障碍期权定价模型的国内外研究动态,确定了本文的定价方法。其次,为了满足投资者客制化的需求以及丰富产品种类的设计目标,在确定了标的指数的基础上对产品进行了设计与优化。通过不断调试,确定了产品的参与率、发行规模等具体参数。作为结构化产品设计的核心环节,本文将产品定定价分为固定收益证券定价与双重障碍期权定价两部分。一方面,运用BSM定价模型及其推导公式以及蒙特卡洛模拟对期权部分进行定价分析,两种定价方法的结果相近,验证了期权定价结果的准确性;另一方面,运用现金流贴现模型对固定收益证券部分进行定价,将两部分价格求和加总,得出产品的最终理论价值。在实现定价结果稳健的基础上,本文对该产品的敏感性进行分析,分别分析了向上敲入看涨期权、向下敲入看涨期权对障碍值及执行价格的敏感程度,为后续修改同类型产品的相关参数以及选择更为合理的障碍价格与执行价格奠定基础。最后,本文列举出了本产品面临的外在风险并提出了应对建议,便于产品的发行方进行管理决策。对内嵌双重障碍期权的上证50ETF结构化理财产品优劣势进行分析,并提出了相应的产品推广策略。

关键词： 地铁屏蔽门   平面度测量   结构光   双目视觉   网格交点定位  

摘要： 随着城市轨道交通的发展,地铁出行方式因其舒适、准时、便捷的特点成为当前最主要的公共出行方式。地铁相关配套设施的市场需求随之急剧增长,对其生产质量要求也日益严格。T形下支座为地铁屏蔽门下部支撑组件的一种钢结构体,其平面度大小关乎整个地铁屏蔽门的安装精度、寿命,而当前对其平面度测量方式主要依靠人工测量,测量效率低下导致平面度测量工序成为影响屏蔽门配套设施生产效率的关键工序。因此,以T形下支座为对象,开发一种结构件平面度测量机器人对提高地铁屏蔽门企业的生产效率和质量管理具有极为重要的工程应用价值,同时对于类似结构件的平面度测量具有一定推广和借鉴意义。平面度求解过程,即为待测表面特征点深度信息求解过程。近年来,结构光及双目视觉已被成功应用于三维测距领域。基于此,本文对基于结构光双目视觉的地铁屏蔽门结构件平面度测量方法和测量机器人开发展开了深入研究。首先基于平面度检测技术要求完成了成像系统与双目相机夹具的硬件设计,并对双目相机和机器人手眼进行标定;重点对基于置信度的结构光网格交点定位算法展开了研究。基于双目测距模型对特征点的三维坐标进行测量,运用最小二乘法求解结构件平面度。与基于激光位移传感器的平面度测量方法对比,验证了本文平面度测量方法的有效性与优越性,通过与人工平面度测量效率与成本对比,验证了开发测量机器人的高效性与经济性。本文主要研究工作如下。(1)基于对T形下支座平面度检测要求的分析,对基于结构光双目视觉的结构件平面度测量机器人系统进行了方案设计。搭建了成像系统,并将双目视觉系统集成于机器人,以实现对T形下支座待测表面的自动化成像,完成了机器人、相机和结构光的选型,以及双目相机双目标定与机器人手眼标定。(2)对基于置信度的结构光网格交点定位算法进行了研究。因结构光网格交点与棋盘格角点在几何特征上具有相似性,先采用Harris角点特征提取算法提取网格交点,实验结果表明该方法因鲁棒性较差不适于本应用场景;随后基于霍夫变换的网格交点定位算法求解网格交点,因结构光光线并不为标准直线,网格交点定位精度较差;借鉴Geiger在棋盘格角点提取算法中计算置信度的思想,针对网格结构光几何特征,设计了基于置信度的网格交点定位算法。该算法通过图像预处理、置信度计算、非极大值抑制、基于强度分布复检四步实现网格交点定位。通过对40件待测结构件网格交点提取结果的分析,验证了基于置信度的网格交点定位算法应用于T形下支座的有效性和良好的鲁棒性。(3)对结构件平面度计算算法进行了研究,并对本文提出的平面度测量算法进行了分析与评估。为进一步提高网格交点定位精度,基于网格交点邻域内像素点灰度值呈中心分布的特征,设计了基于高斯拟合的网格交点亚像素定位算法,依次通过粗定位与精定位两步对网格交点进行亚像素定位;然后基于顺序一致约束进行左右目网格交点匹配,基于网格交点二维图像坐标与双目标定、手眼标定结果,进行网格交点三维坐标的计算,最后基于最小二乘法求解结构件平面度。与激光测距传感器、基于霍夫变换网格交点定位算法平面度测量结果进行对比,验证了本文提出的平面度测量算法的有效性与高效性。(4)对基于双目视觉的地铁屏蔽门结构件平面度测量机器人进行开发与测试,分别从抗干扰能力、效率、经济性对该测量机器人进行分析评估。通过实验验证了机器人运动与环境光对机器人平面度测量结果影响极小,在工厂环境下具有较好的稳定性;与人工平面度测量效率对比,验证了平面度测量机器人测量的高效性;最后基于成本核算,验证了开发的平面度测量机器人具有较高的投资回报率。

关键词： 高中英语单元整体教学   结构化设计   创新应用  

摘要： 单元整体教学首先要以培养学生的学科核心素养为目标，发掘单元主题的教学价值，把教学目标与学科素养融入单元教学活动中，从而让学生形成综合性发展。其次，在设计单元课程目标时，教师要先对单元课程展开研究与分类，建立起部分与整体的关联，单元教学目标应具有逻辑关联和进阶性特点。再次，教师要通过对照目标，提出考核任务，教学项目和具体的测评项目应呈现综合性、关联性和实践性的特征，将整合性的教学项目作为实现学生学科水平的落脚点，让学生在各个阶段的多轮教学活动中，逐步建立对本学科主旨含义的全面认识，提高自身综合能力。本文从单元整体教学综述展开分析，探究了单元整体教学的结构化设计以及创新应用。

关键词： 安全性质   形式化方法   轨道交通联锁系统   自然语言处理  

摘要： 安全性质是描述软件系统在各种运行场景下必须要满足的环境条件和功能要求。安全性质的违反可能会引起恶劣的后果,特别对于嵌入式控制系统而言,违反安全性质甚至可能产生难以挽回的结果。因此,对安全性质的验证一直是嵌入式控制软件开发过程中重要的一环。对于安全性质进行形式化的验证是一种可靠的保障嵌入式控制系统安全性的方法。然而,形式化方法基于形式化语言和形式化模型,而目前的工业界中,由于自然语言描述实际场景的丰富性和形式化的高门槛,工程师仍使用自然语言来编写安全性质,这意味着如果想要将基于验证的形式化方法用于安全性质验证中,必须先对自然语言进行形式化转化。而自然语言因为其多变复杂的句式和语法,使得自动化地对其进行形式化转化显得格外困难,是该领域学术研究的一大挑战,也是许多嵌入式控制系统行业的一大技术壁垒。 本文提出了一种基于依存关系分析的自然语言处理技术自动生成安全性质的方法,选用在嵌入式控制系统中具有代表性的轨道交通联锁系统作为研究的对象,本文为联锁系统的自然语言安全需求自动化地生成了安全性质,并在实际的验证工具上对本文生成的安全性质进行了验证,证明了本文提出方法的可靠性和实用性。本文的主要贡献是: 1)提出了一种基于依存关系分析的知识图谱生成方法,通过三元组的抽取和精化合并来获得自然语言需求中的实体间关系和属性,该方法支持从自然语言需求中半自动化地生成以三元组和二元组形式表示的知识图谱。 2)提出了一种基于依存关系分析的安全性质生成方法,通过归纳出联锁系统需求的依存关系间的规则来完成对自然语言中语义信息的抽取和组合,该方法支持从自然语言安全需求中自动化地生成的准确可靠的安全性质。 3)设计并实现了安全性质生成工具,可对给定的需求文档生成知识图谱以表示领域知识,并对给定的自然语言安全需求进行安全性质生成。本文将生成的安全性质在真实工程中进行了性质验证,证明了生成性质的有效性和准确性。