教学课程资源库 更多>>

关键词： 汽轮机控制保护系统   形式化方法   时间自动机   活性   UPPAAL  

摘要： 随着电力系统智能化程度不断提高,其面临的安全隐患也在日益增加,电力系统在提供高质量电力资源的同时,还需要满足日益提升的安全性要求。作为电力系统的主设备之一,汽轮机的安全性是整个电力系统安全、平稳运行的前提,而汽轮机控制保护系统又是实现这种安全保障的关键。传统控制领域的微分方程或差分方程模型只用于刻画系统的输入输出以及内部状态之间的关系,无法刻画系统的完整运行逻辑,这对汽轮机控制保护系统这类实时逻辑系统的研究极为不利。 针对上述问题,本文提出了一种基于时间自动机的汽轮机控制保护系统模型。在此模型基础上,揭示了形式化方法中的活性与汽轮机控制保护逻辑的内在联系,将逻辑完整性问题转换为活性完整性问题,进而提出了状态检测和变量检测两种活性完整性的检测方法。此外,本文还研究了一种针对汽轮机控制保护逻辑的攻击方式。本文的主要研究成果如下: 1.针对传统模型逻辑刻画困难、无法完整描述系统动态过程的难题,本文采用时间自动机的方法,提出了一种汽轮机控制保护系统的形式化模型。该模型使用时间自动机的多元数组描述汽轮机控制保护系统中每个不同设备的状态及其状态转换过程,并且通过积处理,将不同设备的自动机模型进行同步。通过UPPAAL下的仿真实验,验证了模型的准确性。 2.针对汽轮机控制保护系统的时间自动机模型对控制保护逻辑描述不够清晰的问题,本文基于标签转移系统的方法,通过对安全性和活性两种特性的研究,揭示了形式化模型中活性与汽轮机控制保护逻辑的内在联系,将控制保护逻辑完整性问题转换为活性的完整性问题。进而,提出了状态检测法和变量检测法用于检测活性的完整性。最后,在UPPAAL验证器的帮助下,验证了检测方法的有效性。 3.针对现有控制保护逻辑的脆弱性,提出了一种针对汽轮机控制保护逻辑的攻击方式,其主要由控制逻辑攻击和保护逻辑攻击两类组成。两种攻击分别通过篡改控制指令参数和传感器监测阈值的方式破坏系统控制保护逻辑。基于攻击机理,采用时间自动机的方法分别对两类攻击建模,得到其形式化模型;最后通过与正常系统模型间的联合仿真实验,验证了攻击的危害性。

关键词： 列车运行控制系统   形式化方法   基于模型的开发   需求规范   建模验证  

摘要： 列车运行控制系统是保障列车安全与高效运行的核心。目前中国列车运行控制技术整体已步入世界先进水平，正在向智能化、智慧化方向发展，迫切需要以自主化工具平台支撑的正向研发设计方法。形式化方法是保障列车运行控制系统功能正确实现的关键。文章首先回顾了列车运行控制系统的发展过程，分析了计算机时代列车运行控制系统的特点；总结了国内外列车运行控制领域形式化的应用研究、取得的进展和趋势，并对比了国内外列车运行控制领域形式化研究的差异；最后提出了采用基于模型的系统工程方法进行列车运行控制系统正向设计的发展方向，并从系统正向顶层设计、形式化技术自主化和人才队伍培养方面给出了发展建议，力求实现功能强大、覆盖全面、性能先进的列车运行控制系统。

摘要： 结构化教学即每节体育实践课的教学应该创设真实的、丰富的体育与健康学习情境，“包括结构化的运动知识和运动技能、体能、展示或比赛、规则和裁判等”[1]。本文从课堂教学的角度，通过水平五篮球模块“半场人盯人防守战术配合”课例的呈现，从体育结构化教学角度开展探索实践。在体育与健康课堂中落实结构化教学，既要处理好学生运动知识和技能的已有经验与新授运动知识和技能之间的关系，同时还要从整体把握，

关键词： 形式化方法   系统建模   XYZ/ADL   模糊系统  

摘要： 随着科技的不断发展,计算机软硬件系统在商业、金融和工业等多个领域都占据了举足轻重的地位。由于系统实时处理能力的不断提升,这些系统逐渐变得更为复杂,从而在验证其精确性和稳定性方面面临着越来越大的挑战。计算机软硬件系统在各个相关领域都有广泛应用,如交通管理、电子商务、载人航天以及核安全控制等关键系统,一旦系统发生故障,可能会导致无法预估的严重后果。因此,确保计算机软件和硬件系统的准确性与可靠性变得至关重要。为满足计算机软件和硬件系统的需求,需要建立准确的定量模型。这种模型通常基于物理量的变化趋势、范围等定量属性,以及相应的定量时序逻辑,如时间约束和数量限制。将这些属性和逻辑整合到系统模型中,可以更加准确地描述系统的行为和特性,从而提高系统的可靠性和正确性。然而,在某些情况下,系统的规范和约束可能包含模糊或不确定的信息,所以利用传统的定量模型系统方法会无法胜任验证模糊系统的工作。为了解决这个问题,本文将模糊理论与形式化验证方法相结合,以应对系统中存在的不确定性和不可靠性,并且在现有研究的基础上,探讨了形式化语言XYZ/ADL和模糊系统相结合的建模问题。本文主要的研究内容如下:(1)介绍了模糊系统和形式化技术的结合方法及其应用于主流计算机软硬件系统的现状,提出了改进此类技术以应用于构建系统模型的思路。(2)提出了一种模糊系统建模方法,采用形式化方法语言XYZ/ADL对模糊系统进行建模,并根据这思路,给出了一套模型和验证分析的方法,有效地实现了模糊系统建模的自动化和高效化。通过引入形式化方法,解决了之前模型构建遇到的不准确和不可靠的问题。(3)为证明提出的建模方法在真实环境中的可行性,本文以升降梯为例,采用了XYZ/ADL形式化语言对其进行了全面的功能规范、结构模型、动态模型和运行模型的描述。通过研究结果表明,本文提出的基于XYZ/ADL的形式化模型能够精确地解析模糊系统中复杂组件之间的关系,准确模拟系统状态,为深入理解和预测系统行为提供了可靠的支持。这一研究为进一步完善形式化验证方法和技术提供了有益的启示,为确保软硬件系统的准确性和可靠性奠定了坚实基础。

摘要： 在“第九届中小学优秀体育与健康教育课教学观摩展示交流活动”（以下简称“本届展示活动”）中，笔者执教的高二《篮球：持球三威胁——运球进攻》一课作为自定教材进行现场展示，结合前期备课、磨课的设计思路，就如何基于模块视角，以学科大概念为核心，以主题为引领，使课程内容结构化，实现学习内容的有趣、有用，取得了较好的课堂教学效果。一、知识与技能结构化设计思路1.逆向拆解形成篮球项目模块“大结构”

关键词： 结构化理财产品   碳金融   碳排放权   清洁出行   蒙特卡洛模拟  

摘要： 2021年,中国正式提出碳达峰、碳中和的“双碳”政策目标,该目标的提出意味着碳金融将会成为未来中国金融市场的重要组成之一。各大金融机构也意识到碳金融的重要性并不断开发与完善碳金融产品。然而,目前碳金融市场仍存在资金缺口巨大、产品种类不足等一系列问题。基于以上背景,本文结合低碳政策导向,聚焦清洁出行领域,设计出一款将资金投资于广东省的碳金融结构化理财产品。本产品的设计过程主要可以分为三部分,第一,产品设计前的准备阶段,首先,该部分主要是对相关的研究进行介绍,为产品的后续设计提供理论依据。其次,细分产品的定位,对目前产品面临的市场环境和客户进行调研,了解市场与客户的需求,得出该产品设计的可行性。第二,产品设计的构建阶段,设计一款以21深圳地铁MTN004(碳中和债)和碳排放权为挂钩标的的结构化理财产品。完成设计方案后对产品进行定价,固定收益部分使用现金流贴现进行定价。衍生品部分以广东省碳排放权前1年收盘价作为定价数据,使用GARCH模型估计波动率,估计得出广东碳排放配额(Guang Dong Carbon Emission Quota,GDEA)年波动率为0.2214。在此基础上分析资产价格概率分布,运用蒙特卡洛模拟出资产价格的所有可能变化路径,并贴现出期权部分的价值。最后综合两个部分确定本款理财产品的理论价格。第三,产品设计后的分析阶段,产品设计完成后,需要对该款产品的优势进行对比分析、对内外风险进行揭示,以此来进一步反推产品的可行性。最后基于上述分析,从产品、渠道和品牌三方面为产品设计出一套比较合理的营销策略。经过分析,本文最终得出了一款收益为1.2%+的保本浮动收益6个月期碳金融理财产品,预期收益率为2%左右。产品带来的碳减排量约为105吨。

关键词： 系统建模语言   状态机   模型转换   ATL   Uppaal   时间自动机   形式化方法  

摘要： 状态机图是系统建模语言(SysML)中的一种建模视图,它可以描述一个系统的行为,已被广泛应用于模型驱动领域。形式化方法作为一种基于数学的技术,可以用来验证软件系统或硬件设计的正确性、可靠性和安全性。本文通过将系统建模语言中的状态机图转换为Uppaal时间自动机,将形式化方法引入模型驱动开发领域,这样可以在软件开发生命周期的早期阶段,对系统进行形式化验证,从而增强系统的稳定性。本文给出了两个模型之间元素的映射规则,开发了一个自动转换工具用来直接将系统建模语言中的状态机模型转换形式化的Uppaal模型。在本文的最后,通过了两个案例来实践本文的方法和工具,证明了该方法的可行性与自动转换工具的正确性。通过模型转换的方法可以有效地利用形式化验证技术的优点,来确保系统的正确性和可靠性。直接地转换模型不仅可以降低开发者的学习成本,也能将形式化方法推广到更多的领域。本文的主要贡献可概述如下:·提出了一种SysML状态机图转换为Uppaal时间自动机模型的映射规则,对SysML状态机图的常用元素进行元素映射,映射为Uppaal时间自动机模型中的元素,为了保证模型转换前后的语义一致性,在元素映射时,考虑了源模型元素的定义,使用目标模型中相同语义元素完成映射。·根据SysML状态机图(源模型)和Uppaal时间自动机(目标模型)的定义,设计了SysML状态机图和Uppaal模型的元模型,使用Ecore模型对两个元模型进行了描述,并且用ATL模型转换语言开发了自动转换工具。·使用“士兵过河”和“时间敏感网络”两个案例展示了包含SysML状态机建模、转换为Uppaal模型和转换后的Uppaal模型的形式化验证三个流程,证明了所提出方法的可行性与转换工具的有效性。

关键词： 黄河风   德育课程   结构化设计   实践活动  

摘要： 我校以“弘扬中华传统文化，培养有根有魂的中国人”为核心德育理念，从“黄河魂”修身课程、“黄河诵”阅读课程、“黄河功”健体课程、“黄河韵”艺术课程、“黄河印”劳动课程五个方面，探讨“黄河风”与小学课程资源的融合，以“必修课程+选修课程+学生社团+实践活动”的立体化设计方式，构建校本化“黄河风”农村小学德育课程体系，有效培养学生国家认同感和责任心。

关键词： 预应力筋   腐蚀防护   电隔离   锚固体系   密封性能  

摘要： 自预应力技术发展至今,由于预应力筋的腐蚀问题造成了巨大的经济损失并严重危害人民安全,国外提出的电隔离防护技术,通过将预应力筋完全封装达到隔离外部腐蚀介质,实现有效的腐蚀防护,同时兼具腐蚀监测。为了提升现有预应力锚固体系的防腐能力,本论文基于电隔离防护方法,改进和优化常规锚固体系的结构,设计了一种电隔离预应力防腐体系结构,并通过试验测试电隔离防腐体系的密封性能和电隔离性能,主要开展的工作如下:(1)对预应力筋腐蚀机理进行研究。分析预应力筋腐蚀的类型和原因,归纳造成预应力筋腐蚀的关键腐蚀介质以及预应力混凝土结构内部需要重点防护的区域,为电隔离预应力防腐体系结构设计提供理论依据。(2)设计研究电隔离预应力防腐体系结构。从防腐、绝缘、密封和力学性能等需求出发,提出设计要求并制定了设计方案,在常规锚固体系的结构基础上,针对腐蚀介质经常入侵的区域分别设计了防护构件,构件包括:保护罩、隔离垫、塑料内衬套、管道密封连接头,基于Solidworks软件建立所有构件的三维模型,并使用ANSYS Workbench软件对关键构件进行有限元分析,根据仿真结果对构件结构进行优化,最后完成电隔离防腐体系三维模型装配和样品试装检验。(3)针对关键构件和整体组装件开展了性能测试试验。其中对单个保护罩构件进行了抗压试验,试验表明保护罩能抵抗的油压超过1.5MPa,满足工程使用要求,验证了前期有限元分析结果的合理性;对体系中的关键密封组装件进行了正压试验和负压试验,在维持30分钟的0.5bar和-0.5bar的气压下,组装件未发生泄露或渗透的情况,验证了设计的体系结构密封性能满足要求;对体系整体组装件进行了28天的电隔离监测试验,监测周期内预应力筋和钢筋间的电阻值均大于15 kΩ,满足fib bulletin75的要求,验证了设计的体系电隔离性能满足要求,最终表明本文设计的结构达到了电隔离防护技术的要求。