教学课程资源库 更多>>

关键词： 高中化学   核心素养   结构化教学   设计策略  

摘要： 高中化学是学生学习的一门重要科目。在我国教育观念持续优化与升级的背景下，教师应革新教学观念，利用结构化的单元授课模式来进行丰富趣味的高中化学教育活动。围绕学科素养来进行高效的化学授课活动;引导高中生积极参与，充分调动他们的潜在能力;激发高中生的主观能动性，指导他们形成积极正确的学习方式和习惯，构建良好的化学思维;通过化学思维应对现实生活中的问题，从而实现学以致用的授课目标。

关键词： 信息物理生产系统   形式化方法   模型-数据双驱动   工厂领域建模   系统验证  

摘要： 个性化定制的多品种、变批量生产模式推动了生产领域的产业细分化、产品多样化、制造服务化等发展趋势,因此对制造领域生产线系统带来的冲击与挑战聚焦为交付时间的骤减、制造任务更加频繁多变和制造需求更加复杂等问题。本文研究个性化定制信息物理生产线的形式化建模与验证方法,通过对具有系统模型交互层次多、生产模型时间跨度大等特点的个性化定制生产线信息物理要素进行统一精确的刻画,建立符合标准的工厂领域(Factory Domain,FD)形式化方法,构建智能工厂领域生产线组件之间资源的即插即用等动态交互行为的形式化模型,以确保个性化定制信息物理生产线各功能属性满足设计要求,从而实现个性化定制生产线组件在多粒度系统层面的模型分析、验证以及部署等过程。主要研究内容概括为以下四个方面:(1)提出了一种可信工厂领域的形式化方法框架。通过分析工厂领域形式化方法的设计需求与设计目标,提出了个性化定制信息物理生产线标准化组件描述的相关概念;基于组件划分的概念集成模型驱动工程的方法与数据驱动的理念,提出一种基于模型-数据双驱动(Model-Data Driven,MDD)的可信工厂领域形式化方法框架;对系统设计时所面临的形式化建模、验证以及性能分析等问题,基于上述框架构建了面向特定领域的形式化方法与支撑工具链,满足了工厂领域信息物理生产线形式化方法中的多维度可信建模需求与异构资源融合的实时验证需求。(2)提出了工厂领域信息物理生产线形式化建模方法。一方面对信息物理生产系统(Cyber-Physical Production Systems,CPPS)个性化定制生产线组件所包含的元素进行组件的规范性划分,提出了基于可扩展形式化过程描述(Extended Formal Process Description,EFPD)的生产线组件半形式化建模方法,直观刻画了生产线组件中产品、工艺、资源概念以及三者之间的交互行为。另一方面,分析了信息物理生产线运行逻辑与特性,定义了个性化定制工厂领域形式化建模语言。以此为基础,基于AutomationML数据交换格式构建了工厂领域的形式化元模型与模型,保证了生产线形式化语义的统一性和模型的可操作性。(3)提出了基于工厂领域生产线动态与静态资源信息的形式化验证机制。通过对功能性验证相关属性的描述,提出了功能性验证相关的量化指标,使用时间有色Petri网作为针对领域形式化模型实施验证的计算模型,实现了对包含产品订单信息、资源实时状态信息的信息物理生产线系统模型的仿真和验证分析。模型验证结果证明了所构建的验证模型提高了生产系统的形式化抽象,满足了生产线层系统在设计时的各功能属性。(4)提出了一种基于形式化机理的信息物理生产线动态系统数字孪生(Digital Twin,DT)建模与性能分析方法,开展了生产线在内外部扰动作用下的自适应运行机制研究,在团队前期构建的原型实验平台基础上,基于MDD生产线建模方法和运行管控工具模块,建立了形式化机理驱动下的物理系统仿真与数据驱动下的信息系统决策之间的映射关系,实现了生产线/制造单元的模型校验、参数修正、性能预测与分析。综上所述,本文以个性化定制信息物理生产线为研究对象,提出了在外部需求或车间资源多变场景下即插即用信息物理生产线的形式化方法相关理论,提升生产线系统的开发效率,降低系统开发成本,避免因个性化定制生产造成的逻辑缺漏与意外故障等时间或经济损失,具有重要的理论与实际应用价值。

关键词： 区块链   智能合约   形式化方法   机制设计  

摘要： 区块链是一项融合多种底层技术的交叉应用技术,其中最为核心的技术包括密码学、分布式计算和机制设计。密码学和分布式计算主要解决区块链的数据存储、通信问题,而机制设计对解决因区块链P2P网络节点具有较强社会属性而产生的一系列问题起到至关重要的作用。这些问题通常分布在区块链的共识层、激励层和智能合约层。近年来,区块链智能合约系统（Blockchain Smart Contract System,BSCS）迅速发展,智能合约作为运行在区块链分布式网络中的计算机程序极大地拓宽了区块链技术的应用领域。目前,业界对智能合约尚且缺乏统一的形式化定义,导致合约复用性低、数据冗余;现有主流共识机制对BSCS适用性较差,易造成计算资源浪费、记账权集中化;智能合约的匿名性、一次交互性导致违约追责难以实现,恶意合约上链可能性增加。为了解决上述问题,本文面向区块链智能合约系统的机制设计问题展开研究,主要研究内容如下:（1）基于条件响应与有限状态自动机的智能合约形式化研究。基于有限状态自动机理论,从逻辑角度剖析智能合约的执行过程,以有向无环图对智能合约进行形式化描述;研究环境对智能合约执行过程的影响,包括合约状态迁移、条件触发机制,建立智能合约的变量-状态-触发器（VST）模型;以一份现实房屋租赁合同为例,使用VST模型描述基于该合同创建智能合约,及其部署、执行、完成的生命周期。（2）基于智能合约领域交互程度的共识机制研究。考虑到BSCS中智能合约应用于多个领域,设计算法求出合约创建节点在某一个或多个领域的交互度,以证明节点对区块链网络的贡献,在此基础上设计交互度证明机制（PoE）以分配记账权。通过仿真实验测试PoE机制在相同设定下与主流共识机制的对比表现,实验结果表明PoE机制相较于PoW、PoS具有更强的灵活性。（3）基于信誉值的智能合约系统激励机制研究。在（1）、（2）两个研究内容的基础上,基于VST模型定义智能合约完成度,以此作为BSCS中节点信誉值的计算依据。为了降低恶意合约上链成功的可能性、提高优质合约上链概率,基于信誉值设计陪审团机制,通过实验模拟持有不同行动偏好的节点（对抗节点、理性节点、诚实节点）在三种不同占比分布下（均匀分布、正态分布、指数分布）的行动,结果表明,陪审团机制在多数情况下表现出对抗鲁棒性,提高了优质合约上链概率。本文对BSCS的共识层、激励层、合约层展开研究,从软件工程、机制设计的角度,对智能合约进行形式化建模,对BSCS的共识机制、激励机制进行设计和改进,结果表明本文所提出机制在优化记账权分配、激励节点行为方面起到积极作用。

关键词： 信息物理融合系统   AADL   Modelica   析错随机混成自动机   规范挖掘   Shapelet  

摘要： 信息物理融合系统(Cyber-Physical System,CPS)是一个描述物理与信息系统相结合的综合系统。随着对CPS的深入研究,人们对嵌入式系统描述需求愈发提高。针对组合建模的方式,本文将AADL与Modelica进行结合,组合成新的建模语言,通过模型转换方法将AADL与Modelica组合的半形式化模型转换为形式化模型,对嵌入式系统进行建模。针对黑盒系统建模的方式,本文采用规范挖掘技术,通过系统运行轨迹描述系统的行为,帮助设计人员灵活高效地了解CPS的行为。 本文主要研究贡献如下: (1)针对CPS系统中离散信息系统和连续物理系统交互融合的混成特性,对CPS进行建模,并使用AADL对CPS的信息资源进行建模,针对CPS不确定性和运行时可能出现故障的状况,提出析错随机行为附件FASBA子语言;使用Modelica对CPS的物理资源进行建模,结合故障树对系统运行时出现的故障进行分析描述。本文通过端口通信,将AADL与Modelica进行连接,并且将AADL、Modelica和故障树进行组合,形成新的完整的CPS模型。 (2)针对形式化模型的应用,将自动机作为形式化模型,根据CPS的不确定性和运行时故障的问题,对混成自动机扩展随机性与故障分析两个属性,并且针对CPS的建模方法,给出自动机的组合规则,提出析错随机混成自动机FASHA。根据半形式化建模语言与FASHA的特性,提出将AADL与Modelica分别转换为FASHA模型的转换方法,并对模型进行验证和故障分析。 (3)针对黑盒系统难以人工建模,本文在Shapelet技术的基础上,对已有的规范挖掘技术进行改进,并提出改进的算法EHATSS,通过将运行时产生的时间序列信号轨迹进行预处理、分段、相似性处理、归类、聚类、离散状态序列和状态变迁挖掘以及变迁跳跃条件和流条件的挖掘,生成自动机,描述系统的行为规范,并针对案例对提出的算法进行验证。

关键词： 形式化方法   定理证明   矩阵   代码生成   Coq  

摘要： 矩阵代码的安全性需求要求对矩阵以及矩阵算法进行形式化,这是软件安全领域中的一个重要研究课题之一。对矩阵计算性能的需求使得矩阵代码日益复杂,这增加了发生代码错误的风险,现代并行硬件通过分块矩阵来实现矩阵运算以提高矩阵运算效率,通常分块矩阵的实现代码比普通矩阵代码更加复杂、难以理解,因此,需要通过形式化方法来对该优化的等价性进行验证。基于通用定理证明器的验证技术虽然不能自动进行矩阵性质验证,但是可以在人机交互的方式下完整的证明矩阵的各种性质,甚至可以证明矩阵代码的完全正确性。本文的第一部分工作是在Coq定理证明器中提出了分块矩阵形式化方法,并证明了分块矩阵与矩阵运算的等价性,最后提出了矩阵与分块矩阵的形式化库,为相关领域其他研究人员进行矩阵形式化方向的进一步深入研究奠定了基础。 在定理证明器中实现的矩阵算法通常是函数式的,函数式的矩阵代码运行效率低下,但其相比于命令式的矩阵代码更容易验证代码的正确性。针对并行硬件的命令式的矩阵代码编写需要专业人员实现,程序的正确性难以得到全面的验证。因此,为了使得矩阵算法在保证正确性的情况下提高其性能,需要将函数式的矩阵代码通过某些规则转换成命令式的矩阵代码。为了保证转换后生成的代码的正确性,代码转换过程需要经过形式化验证。针对该问题,本文在Coq定理证明器中实现了由函数式到命令式的矩阵代码转换技术,并且正在开展形式化验证工作。这项工作为深度学习代码编译器的形式化验证奠定了基础。 本文主要的贡献如下: 第一,本文完善了基于记录类型的矩阵形式化方法,矩阵形式化方法的基础上实现分块矩阵形式化方法,其能够实现将大矩阵运算转换为多个小矩阵运算,在后续有关于分块矩阵形式化证明工作中,不仅证明了分块矩阵运算的正确性,并将矩阵形式化中已证明的性质移植于分块矩阵形式化库中,最后建立了基于不同类型的分块矩阵基础库。 第二,针对函数式代码运算效率较低的问题,本文在Coq定理证明器中实现了一种能够将函数式矩阵代码转换为命令式矩阵代码的技术,该技术中使用连续传递翻译原理和大量重写规则来实现代码转换,其生成的并行命令式矩阵程序的性能比普通顺序执行的矩阵程序的性能有大幅提升。 第三,为了保证命令式代码生成的正确性,本文在Coq定理证明器中对代码转换过程中使用的部分重写以及优化规则进行形式化验证,该验证能够在一定程度上保证经过这些规则生成的命令式程序的可靠性,从而形成一个高可信的矩阵代码生成技术。

关键词： 基于模型的安全分析   模型检查   故障建模   BIP(行为交互优先级)   形式化方法  

摘要： 近年来,我国航空工业的发展速度迅猛,人们的日常生产生活中使用民用航空飞机的频率越来越高。从商用的客机、货机及客货两用机,到通用的农业机、林业机、巡逻救护机、支线运输机等。这些民用航空飞机在带给人们便利化生活的同时,也伴随着风险。一旦其中的软硬件系统出现故障,轻则使用户的财产受到损失、重则造成人员的伤亡。因此,安全性和可靠性是航空工程师在设计与研制民用航空飞机时需要重点关注的。形式化方法是一种基于数学理论的,用于保证系统设计开发与验证过程中的安全性与可靠性的方法。工程师通过使用形式化方法,可以为需求提供形式化规约、为系统建立抽象形式化模型以及为系统模型提供形式化验证,从而提高对象系统的安全性和可靠性。因此使用形式化方法为航空领域的控制系统提供建模与验证支持是可行的,也是主流的趋势和愿景。另一方面,作为研制民用航空飞机时确保安全性和可靠性的标准,国际自动机工程师学会(SAE International)发布的航空航天信息报告6110(AIR 6110)介绍了对民用机载系统和设备进行安全评估过程的指南和方法。AIR6110为航空控制系统架构的安全评估过程提供了指导性的原则,通过安全评估的结果指导架构设计,最终获得满足安全要求的航空控制系统架构。然而,该标准在工业领域的实际应用存在困难,原因有两点:(1)AIR6110并未明确给出安全评估过程所采用的具体技术,加之在系统架构层面缺乏精确的常态及故障模型,使得目前落实AIR6110的主流手段仍然是手动且非形式化的方法,工程师需要投入大量精力手动进行系统建模及安全评估,使得安全评估过程高度依赖工程师的能力与经验,其结果具有主观性,代价高且质量无法保证。(2)系统模型与故障模型的分离,使得安全工程师关注的故障信息无法体现在系统模型中,某些由于架构设计导致的,通过组件间交互生成的深层次故障容易被忽视。针对上述问题,本文提出了一种面向航空控制系统的,以形式化方法为理论基础的行为故障建模及验证技术。我们使用形式化方法为系统在架构设计层面建立系统模型,同时通过系统故障行为生成故障模型,并将两者结合为统一的扩展系统模型。通过将形式化验证方法应用于该扩展模型上,我们可以在最早的设计阶段就确保设计中必要的安全属性,并逐步细化模型特定的细节。我们以AIR6110中介绍的民用飞机车轮制动系统为研究对象,验证了我们的方法可以为航空控制系统领域的安全评估过程提供自动化支持,在降低成本的同时提高了安全评估的效率与质量。本文主要工作包括以下几个方面:·基于行为交互优先级(Behavior Interaction Priority,BIP)的行为故障建模方法提出了在系统架构层面的基于BIP的行为故障建模方法。在特定的航空控制系统领域,有别于传统的非形式化系统模型与故障模型分离的建模方法,我们提出的方法能够基于BIP语言,建立包含架构与故障行为信息的、统一的形式化故障模型。·BIP故障模型的形式化验证对形式化故障模型采用基于仿真执行的统计模型检查方法进行验证。在航空控制系统架构层面,有别于传统的人工检查方式,应用在形式化故障模型中的基于仿真执行的统计模型检查方法能够有效提高安全评估效率并指导架构迭代过程。·模型验证工具SBIP的拓展对模型验证工具SBIP进行了自动化故障建模方面的拓展。在SBIP工具的基础上实现了支持本文所介绍的故障模型生成过程中的故障组件生成、故障注入功能的插件。

摘要： 桥梁的工程结构美学在某种程度上比较依赖其背后的结构体系以及建筑材料,故在进行桥梁设计时,要考虑其使用过程中的稳定性以及年限,以及解决如何将结构面上的承载体进行有效的化解并且将整体的结构形态呈现出相应的美学等问题。木质结构体系下桥梁设计效果图。桥梁的外部立面是其展示的形体,在其外部形态中内部是其核心的支撑点,也是整体结构力学的出发点,故在设计与建造桥梁时,要注重其外部形态中内部结构的建造。整体的桥梁采用木质体系,究其原因,木质具有较好的可塑性、柔韧性,

关键词： 多孔锌负极   锌枝晶   副反应   应力释放   金属锌电池  

摘要： 可再生清洁能源的开发与利用,对降低传统化石能源的消耗,缓解其所带来的环境问题和创建可持续的生态环境具有重要的战略意义。电化学储能设备可以将风能、太阳能等可再生能源进行存储,是构建高效可靠的电力系统的重要组成部分。锂离子电池由于具有高的能量密度和长循环寿命,在便携式电子设备市场占主导地位,并逐步渗透动力汽车市场。然而,一方面全球范围内的锂资源短缺导致锂离子电池无法满足日益增长的需求;另一方面锂离子电池存在的安全问题严重影响其大规模的应用发展。水系锌离子电池采用金属锌作为负极,它具有储量丰富、无毒性、高安全性、高的理论体积比容量(5855 mAh cm)、低的电极电位(-0.762 V vs.标准氢电极电位（SHE）)等优点被认为是最理想的负极材料之一。尽管水系锌离子电池作为大规模储能装置系统的理想候选材料引起了高度的重视和广泛的研究。但水系锌离子电池在商业化应用过程中,仍需解决锌金属负极的几个重要科学问题:（1）电池循环过程中锌枝晶的生长,会刺穿隔膜导致电池短路,降低电池的循环寿命;（2）金属锌在水中的热力学不稳定性会导致其发生腐蚀和钝化,严重阻碍了锌离子的扩散;（3）金属锌作为负极在电池充放电过程中会发生析氢反应,使电池发生膨胀甚至开裂的风险。因此实现金属锌负极稳定且高效的可逆循环是解决锌金属负极问题的关键因素。本论文立足于锌金属负极的结构化设计,一是研究了三维多孔锌金属负极结构与抑制锌枝晶生长的构效关系;二是采用结构化设计与界面修饰的协同作用,抑制锌枝晶生长的同时有效抑制副反应的发生,提升了水系锌离子电池的电化学性能。主要的研究结论如下:1.利用激光蚀刻方法制备了垂直均匀孔结构的锌金属负极（LVP-Zn）。通过调控LVP-Zn负极的孔径和孔间距的大小来研究锌的沉积行为,均匀垂直的孔结构可以有效的降低电极表面的电流密度,使得金属锌均匀的沉积在孔结构中。在表面包覆的聚酰亚胺胶带（PI）可以有效的抑制副反应的发生。在LVP-Zn电极沉积锌后,组装的对称电池可以在0.2-5 m A cm的电流密度下进行稳定的循环,并且与正极材料Mn O组装的全电池在1 A g电流密度下可实现270 m Ah g的高比容量和高的容量保持率,展现出优异的电化学性能。2.通过金属网辅助压延法与Nafion涂层相结合制备了Nafion修饰的图案化锌负极（N@P-Zn）。通过理论计算和原位观察研究了金属锌沉积过程中应力的产生与锌枝晶生长的关系。制备的图案化凹槽结构锌负极可以有效的释放锌沉积过程中引起的应力变化,抑制枝晶的生长。在此基础上,通过将图案化结构锌负极与Nafion相结合得到N@P-Zn复合负极,研究了Nafion涂层抑制副反应的作用。将N@P-Zn电极组装的对称电池,在10 m A cm的高电流密度下,可以稳定循环1200 h,且电压极化较低。组装的柔性全电池可以提供约186 m Ah g的高容量,且可以稳定循环超过150次,在不同弯曲状态下依然可以进行工作,具有良好的机械稳定性能。