教学课程资源库 更多>>

摘要： “文学阅读与创意表达”隶属于发展型学习任务群，对接的是“审美创造”这一语文核心素养。《义务教育语文课程标准（2022年版）》（以下简称《课程标准》）指出：“本学习任务群旨在引导学生在语文实践活动中……表达自己独特的体验与思考，尝试创作文学作品。”为了践行并达成上述宗旨，教师在设计学习内容时要树立结构化意识，借助任务情境的精心创设、学习资源的有效整合、学习策略的对比筛选、学习工具的建构运用等多维途径，认真组织语文教学活动，切实促进学生审美创造素养的发展。

摘要： 为落实《义务教育体育与健康课程标准（2022年版）》[以下简称《课程标准（2022年版）》]要求的“设计专项运动技能的大单元教学”，按照“2022年度四川省中小学体育教师现场课展评活动”要求，笔者所在区域报送了水平二（四年级）《田径运动大单元》（第7课时）一课，为了更好地设计田径运动（水平二）大单元教学计划和课时计划，由教研员带领成立了磨课团队，并设计了整个大单元教学计划及课例。

关键词： 分支预测   信息流控制   形式化方法   硬件验证  

摘要： 分支预测是现代处理器设计中的一项重要性能优化技术,极大提高了处理器指令流水线的执行效率。近年来以Spectre漏洞为代表的分支预测机制相关安全问题频频出现,表明现代处理器的分支预测器设计存在重大安全隐患。然而分支预测器的设计复杂,传统的测试验证方法效率低下,难以覆盖所有漏洞,基于形式化方法的安全验证成为新的研究热点。本文面向分支预测器安全的形式化验证开展研究,主要创新点和成果归纳如下:1.提出一种基于信息流控制理论的分支预测安全属性定义——预测非干涉,即存在两个安全等级不同的使用者共享同一个分支预测器时,两个使用者之间不能在预测执行的情况下产生比顺序执行更多的额外信息流,并对该属性给出了形式化定义。2.将分支预测攻击描述为一系列分支操作的组合,建立了分支预测攻击的形式化表示。基于这一描述方式,本文分别建模了 Bimodal、Gshare、TAGE、BTB、RSB以及一种通用分支预测器等设计的模型,并阐述了分支预测安全属性的验证方式。3.提出一种使用模型检测技术的处理器硬件单元验证系统,该系统具有适应多种指令集架构、多种硬件单元设计和验证效率高的优点。基于该验证系统对多种分支预测器模型进行验证,发现了一种新的利用分支历史缓冲区泄露分支跳转历史信息的攻击方式。

摘要： 一、教材分析“百分数的认识”是人教版六年级上册第六单元“百分数（一）”中的第一课时内容，百分数是一种特定形式的分数，表示两个数或者两个数量之间的倍比关系。正是这种形式，使百分数能够很方便地进行表达和比较，在生活和生产中有极广泛的应用，尤其在统计时用得很多。2022版课程标准把本单元放入“统计与概率”范畴。

关键词： 安全协议   形式化方法   事件逻辑   秘密性  

摘要： 安全协议是现代网络通信的基础,证明协议的安全性问题是当今研究热点之一。认证性和秘密性是安全协议的两大基本安全属性,在错综复杂的网络环境中,如果安全协议的安全属性没有得到严格的证明,存在于网络通信中的风险将无法预估。目前,对安全协议进行分析与验证最强有力的手段是形式化方法。事件逻辑理论(Logic of Events Theory,LoET)是一种通过定义事件结构对安全协议安全属性进行证明的形式化方法,其中包含事件系统、公理系统、谓词公式和协议的形式化描述。利用事件逻辑理论对安全协议进行分析,只需对定义在协议诚实主体上的事件进行推理即可,入侵者事件不会对推理结果产生影响。本文在事件逻辑理论的基础上,对谓词公式进行定义,结合定义给出一套推理规则,构建事件逻辑秘密性证明系统,并运用扩充后的事件逻辑对两种不同类型协议的安全属性进行证明,使事件逻辑理论应用范围扩大,能对安全协议的秘密性进行证明。本文的主要工作和创新点如下:1.扩充事件逻辑理论谓词公式。在现有事件逻辑理论的基础上,扩充谓词公式来刻画协议主体状态。扩充谓词Has用以刻画主体拥有原子项,并给出相应的定义,为后续事件逻辑秘密性规约奠定基础;扩充谓词Fresh和FirstSend以刻画数据项的新鲜性以及发送事件的首发性,并给出相应的推理规则,增强事件逻辑理论的事件排序能力,降低协议分析过程中的复杂度,使得协议安全属性证明更加简洁。2.在事件逻辑理论中引入迹τ(e1,e2,...,en)的概念,并给出相应的定义。基于迹引入入侵者刻画,利用数学归纳法证明在事件逻辑秘密性证明系统中,证明协议秘密性只需证明协议中诚实的发起者和响应者发送的消息是安全的,而不需要对入侵者可能的攻击行为进行显示推理。3.构建事件逻辑秘密性证明系统。在事件逻辑原有理论基础上,扩充秘密性证明系统,扩充内容包括定义GoodMsg用来刻画Data类消息的安全性;定义GoodSend用来刻画Send事件的安全性,并由GoodSend推广至整个网络得到GoodNet;引入KeyHonest和SecHonest的概念刻画诚实主体的属性;并由以上定义构造一系列推理规则;基于事件逻辑理论给出了秘密性通用的形式化规约公式,使得证明目标更加明确,增强事件逻辑理论的通用性,扩大事件逻辑理论的适用范围。

关键词： GP TEE规范   需求工程   自动验证技术   形式化方法  

摘要： 随着信息技术不断发展,智能移动设备功能也越发强大,但同时移动设备所承载软件的安全性和用户敏感信息的安全性成为该领域的重难点问题。可信执行环境(Trusted Execution Environment,TEE)的提出有效缓解了移动设备领域的安全痛点问题。为进一步提高移动设备厂商所开发软件的规范性与安全性,GP(Global Platform)组织起草并制定了面向TEE的规范和标准。然而由于自然语言歧义性等原因,GP规范与TEE具体实现之间的一致性仍无法得到保证。针对上述问题,本文基于软件形式化方法相关技术理论,首先提出了一个面向GP TEE规范的形式化需求建模框架,然后设计实现了与框架配套的自动化建模验证原型系统,并进一步以OP-TEE作为建模验证对象,通过对比实验论证了所提框架及所设计系统的有效性。本文主要工作有:(1)提出了一个面向GP TEE规范的形式化需求建模框架Tee FRMF,框架核心是一套基于模板引导的需求规约方法TGReq和相应的转换映射规则。TGReq通过限定输入的方式引导用户填充模板,抽取需求规范中的关键结构并过滤次要信息,对数据、专有名词、安全属性以及执行流程和调用关系进行结构化和形式化描述。映射规则将需求规约转化为基于有限状态机(Finite State Machine,FSM)的中间模型,以适应不同的验证后端,增强框架的可扩展性。(2)基于SBIP验证工具,以插件的方式将需求建模功能集成于验证工具,形成一套完备的需求建模和验证原型系统。首先针对BIP验证语言给出了中间模型到验证模型的自动转换算法,进而结合框架和一系列转换规则,实现各功能模块。基于该系统可以实现自动建模和验证工作,极大提升了工作效率。(3)建立了GP TEE基础规范的安全需求规约以及OP-TEE的行为规范并证明了两者之间的一致性。首先通过分析GP规范表达特点,抽取并建立了对应的数据字典和术语表,形成了半形式化的安全需求规约。进一步选择TEE领域的优秀开源方案OP-TEE作为研究对象,利用本文所设计的自动化建模验证原型系统构建了OP-TEE实现层API接口模型、抽象层功能模块模型以及GP TEE安全属性模型,并成功验证了OP-TEE实现与GP规范的一致性。

关键词： 结构化教学   情境教学   单元教学  

摘要： 以“探秘钡盐沉淀溶解平衡”为例，探索以系列真实情境为载体、引领性主题为依托、凸显知识结构化及思维训练结构化的单元教学的设计与实施。

关键词： 苏教版   结构化教学   笔算竖式  

摘要： 文章以苏教版数学三年级上册“两、三位数乘一位数”一课为例，通过计算水平和计算算理的前测，有针对性地设计教学：抛出问题，经历算法多样；展开讨论，讲清算理意义；拓展提升，实现算法迁移；拓展延伸，巩固算理算法.基于前测的结构化的教学注重竖式建模，促进整体认知；注重单元整体教学，重构学习课时.

关键词： 形式化方法   TPZN   车联网   信息传输机制  

摘要： Petri网是形式化验证领域一种重要的建模工具,它具有良好的图形表达功能和严格的数学分析能力,使得系统中进程或部件的顺序、并发等关系表达更加直观。经过半个多世纪的研究,由Petri网衍生出来的各种高级Petri网应用于各个领域。随着无线通信技术、云计算技术和传感器技术等快速发展,车联网这类大型复杂动态系统层出不穷,这些系统在信息时代的地位举足轻重,因此,对这类复杂系统进行形式化建模,并对建立后的系统模型进行分析验证,检测模型的正确性、完整性、可达性等性质至关重要。大型复杂动态系统往往模型结构庞杂,容易因模型状态空间过大导致状态爆炸问题,有色Petri网、时间Petri网、谓词/变迁网等高级Petri网系统虽能有效缓解系统模型的规模问题,但状态空间爆炸问题仍然存在。针对上述问题,本文以车联网信息传输机制为应用背景,围绕车联网信息传输交互过程的形式化建模与验证展开研究。本文主要研究内容包括:(1)针对车联网这类大型、复杂动态系统模型构建时存在状态空间爆炸问题,融合时间Petri网和Z语言的优势,提出扩展时间Petri网和Z语言的TPZN模型,并将它应用于车联网信息传输机制的形式化建模与分析,给出TPZN模型的完整性、可达性和活性分析方法;(2)针对多源异构数据环境下车联网信息传输机制节点数量大,拓扑结构的动态性、信息传输的实时性等特点,基于TPZN对车联网信息传输机制进行形式化建模;利用TPZN-Z语言对车联网信息传输机制模型中的节点设备信息和交通规则进行形式化描述,刻画出模型的功能属性和非功能属性;利用TPZN-TPN构建车联网信息传输机制的信息流模型;(3)针对建立的多源异构数据环境下车联网信息传输机制的形式化模型,利用给出的TPZN模型形式化分析与验证方法,进行模型的完整性、可达性、活性分析与验证,并利用Snoopy软件仿真,分析车联网信息传输机制模型。本文的研究内容及实验结果表明,该形式化方法通过简化系统的网模型结构,能有效避免模型状态空间爆炸问题,以及降低模型的分析复杂度,提高大型复杂动态系统的安全性。