教学课程资源库 更多>>

关键词： 形式化方法   操作系统   数据库   文件系统   分布式共识协议  

摘要： 对高可靠系统软件需求的不断增加使得形式化方法在工业界引起了广泛的兴趣。文章概述了当前主流形式化方法，分析了国内外研究态势，并介绍了形式化方法在设计和实现操作系统、编译器、同步原语、文件系统、数据库系统和分布式共识协议等方面的实践。基于这些实践，进一步总结了形式化方法在系统软件中应用的经验，并从理论和工程两方面讨论其可能面临的挑战，最后针对这些挑战提出发展建议。

关键词： 形式化方法   动态系统   李雅普诺夫屏障证书   混合整数规划  

摘要： 信息物理系统(Cyber-Physical Systems,CPS)是一类集成了计算、通信、控制和传感技术的复杂系统,广泛应用于智能交通、工业制造、航空航天、智能家居等领域。动态系统理论提供了一种数学建模的方法,可以用来描述CPS或其子系统的运动状态和变化趋势,并实现控制和优化。通过动态系统建模,研究人员能够更清楚地了解系统的行为和特征,探索系统的内在规律和机制,从而为系统的设计和控制提供参考和指导,提高系统的可靠性、安全性和效率。但由于动态系统行为的复杂性和不确定性,传统的建模方法面临准确性、效率和可扩性方面的挑战。深度学习技术为动态系统提供了简单、灵活的建模方案,然而其难以解释的特点限制了它在安全攸关领域的应用。形式化方法能在一定程度上弥补深度学习技术的缺陷,该方法通过数学计算和逻辑推理来分析系统的设计并检测潜在的错误和缺陷,为计算机软件系统的正确性提供严格保证。本文针对具有安全性和可达性的动态系统提出了形式化学习方法,该方法结合了深度学习强大的建模能力和形式化方法的严密逻辑来自动学习和验证动态系统模型,确保它们符合预定义的规约——安全性和可达性。其中,安全性是指对于给定系统的初始状态,系统在随时间演化的过程中不会进入不安全状态集;可达性是指系统状态随着时间的推移总能进入目标状态集。本文的研究内容如下:·研究了面向离散系统的形式化学习方法。设计了离散系统的神经网络李雅普诺夫屏障证书(Lyapunov Barrier Certificate,LBC)及其训练方式,LBC是表明系统具有安全性和可达性的通用证书。训练得到的神经网络证书通过混合整数线性规划技术得到验证,这种优化技术可用于解决涉及连续变量和离散变量的数学优化问题。通过将神经网络的验证问题表述为具有二值变量的优化问题并求解,即可判定模型和神经网络证书是否满足规约。实验结果表明,该方法能够成功合成离散系统的LBC,且与DDPG(Deep Deterministic Policy Gradient)相比有更好的长期预测效果。·研究了面向连续系统的形式化学习方法。由于连续系统和离散系统具有不同形式,这导致了李雅普诺夫屏障证书的形式也不同,因此需针对性地设计损失函数。为了验证连续形式下的LBC中的李导数条件,需要采用混合整数二次规划,这种规划技术用于解决包含线性约束和二次约束的优化问题。在实验中,应用这一形式化学习方法成功合成了神经网络证书,且准确地重建了系统的向量场。·对上述两种方法实现了一个形式化学习框架FLMSR。该框架由三个交互部分组成:Learner、Seeker和Verifier。其中Learner用于联合学习动态系统模型和神经网络证书,Seeker对系统状态空间进行采样,通过仿真寻找反例,反例会在下一次迭代中用于更新模型和证书。Seeker寻找反例的方式是算力节约型的,如果这种方式未能找到反例,Verifier将对模型和证书进行验证,以对模型的安全性和可达性提供形式化保证。

关键词： 结构化   小学数学   单元教学设计  

摘要： 结构化教学指的是一种以结构化意识为基础，运用结构化方法，促进学生思维结构层次不断提升的教学模式。数学本身就是一门注重结构的学科，为了让学生的数学思维从低阶迈向高阶，教师有必要基于结构化视角，合理设计单元教学活动。基于此，首先分析了基于结构化的小学数学单元教学设计的价值，随后从知识体系结构化、方法应用结构化、思维引导结构化三个方面着手，探寻了单元教学结构化设计的具体策略，并结合典型案例加以分析，达成理论与实践的协调统一，旨在建构更为高效的小学数学课堂，驱动学生获得更为深远且全面的发展。

摘要： 编者按：“中学数学结构化教学设计与实施的行动研究”是上海市第四期“双名工程”攻关计划虞涛数学基地的攻关课题.课题组提出，结构化教学的基本特征是整体思考、把握本质（用整体的眼光看待学科教学）；内在基础是联系着手、分析关系（剖析学科教学系统内部各要素的联系方式）；根本目标是演绎发展、获取规律（推动学生认知结构的完善与学科核心素养的发展）.本期刊登的是课题组的四篇最新研究成果.

关键词： 形式化方法   安全攸关系统   形式规约   形式分析与验证  

摘要： 形式化方法包括计算系统（软硬件和网络）的规约、构造、分析与验证的数学基础、技术和工具。随着安全攸关系统在国民经济和国防等关键领域的应用越来越多，复杂系统可信性问题日益凸显。形式化方法已经成为开发安全可靠的安全攸关系统的关键技术之一，也是解决中国“缺芯少魂”的核心技术之一，同时也是国际学术前沿。文章回顾国内外形式化方法研究现状，分析国内外研究差距，并提出加强中国这方面基础研发的若干建议。

关键词： 结构化设计   道路设计   桥梁设计  

摘要： 结构化设计是道路桥梁设计的重要内容，可以保证道路桥梁工程施工质量。本文分析了道路桥梁设计中结构设计的必要性，研究了结构化设计在道路桥梁施工中的应用原则，最后说明了道路桥梁结构化设计的应用要点，以期更好地促进我国交通运输业的发展。

关键词： 结构化设计   学习活动   高阶思维  

摘要： 高阶思维，在布卢姆的教学目标分类中表现为分析、评价和创造，具体指向问题求解、批判性思维、创造性思维等能力。《义务教育语文课程标准（2022年版）》强调在语言实践中“发展思维能力，提升思维品质”，并对思维能力的内涵作出了具体诠释：“思维能力是指学生在语文学习过程中的联想想象、分析比较、归纳判断等认知表现，主要包括直觉思维、形象思维、

关键词： 形式化方法   线性时态逻辑   形式语言   联锁系统  

摘要： 模型检查是形式化验证的重要方法之一,在模型检查中,需要对待验证的性质创建形式语言描述的规范说明。本文基于常用的线性时态逻辑LTL(Linear Temporal Logic),提出了一种在有限域上的性质描述语言:有限域上的量词线性时态逻辑FQLTL(Finite Quantified Linear Temporal Logic)。顾名思义,FQLTL用量词和谓词来约束系统中的域,并且使用LTL的时态操作符来描述具有时态的性质。比起LTL,FQLTL更适合描述同时需要限制范围和时态的规范性质,可以被运用到如轨道交通联锁系统等许多实际工业场景中。此外,本文根据FQLTL语言的特性,提出了对其做可满足性检查的方法,并且给出了具体实施的理论依据、流程架构和算法细节。将形式化方法与安全攸关的大型系统结合是非常有意义且被极力推荐的,故本文在提出新的形式化语言FQLTL,给出相关定义和理论的基础上,以足量案例和可实施的实验说明所提出新语言的应用性以及其对相关领域的价值。本文以与轨道交通联锁系统合作的项目做为背景,详细地给出了提出语言的安全需求规范描述到可满足性检查实施的过程以及相应算法架构。将本文所定义的新语言运用在轨道交通系统中,可以覆盖大部分所需的安全规范说明,能够实现对描述出的规范进行可满足性检查,并能够找出一些不满足规范的反例。

关键词： 单元整组作业   结构化设计   小学语文  

摘要： 作业，是学生学习的一种形式，也是教师引导学生学习的载体，能促进学生学习，提高学生学习能力。而目前的语文作业存在整体性不够、层次性不强、持续性不高等问题。对此，笔者试图采用单元整组的方式设计、布置作业，并从锁定单元作业目标、提炼单元重点作业、规划兼顾课与课之间的作业、联系深入课与课之间的作业、巩固运用单元重点作业、制订“围绕式”单元延展作业、推进“围绕式”单元延展作业这几方面进行了实践，效果明显。