教学课程资源库 更多>>

摘要： 在推进中小学体育教育教学改革的过程中，“教会、勤练、常赛”的一体化呈现尤为关键[1]。田径作为义务教育阶段体育与健康课程的必学内容之一[2]，田径教学也应当适应“教会、勤练、常赛”一体化呈现的要求。本文以接力跑教学为例，试图通过单元层面的接力跑教学内容结构化设计和课堂教学层面的接力跑学练内容结构化设计探寻田径跑类项目的“教会、勤练、常赛”一体化教学思路。

摘要： 在“双减”的背景下，如何设计一节知识点精准、学生兴趣浓厚的课成为教师研究的重点课题。笔者尝试向斯苗儿老师提出的“四有”好课靠拢，选择“面积”一课，从“设计前测，摸准学情”“合理选材，贴近单元”“结构化设计，精准教学”这三个角度进行分析，旨在为广大教师提供一个可以借鉴的课例。

关键词： 建模语言设计   汽车控制系统   需求分析   需求确认   形式化方法  

摘要： 嵌入式控制软件作为电子产品中的主体,广泛的应用于诸多领域的控制系统中。而这些系统的安全性和可靠性都依赖这些嵌入式控制系统,如果这些嵌入式设备没有按照预期设计工作,则会导致不可预估的财务损失和人员伤亡风险。经过学术界和工业界的研究和实践,发现由需求着手,将形式化方法引入到需求中,通过从源头上确保控制系统的安全性和可靠性是一种行之有效的方法。但是由于目前对于使用形式化方法来实现从软件的需求描述到软件开发完成代价过大,除了一些对安全要求极高的航空航天等领域外,工业界往往是在软件代码完成后对其进行测试或者形式化验证的方式来提高代码的可靠性。因此需要设计一套能够将形式化方法对一个系统进行建模的工程化方法,并使得这个工程化的方法能够被工业界的开发者接受。为此,本文提出了一套用于引导新能源汽车控制系统的形式化规约和需求确认的形式化工程方法,并且已将此方法试用于与华为合作的项目中。本文主要贡献如下:1)在充分考虑到工业界的具体情况的基础上,提出了一种针对新能源汽车控制系统能够将需求文档中的自然语言向需求模型进行转化的需求形式化建模方法。2)针对新能源汽车控制系统的特征,设计并实现了新能源汽车控制系统领域专用的建模语言VCSDL(Vehicle Control System Description Language)。3)设计并实现了支持针对新能源汽车控制系统需求领域专用的建模工具,该工具可以快速帮助需求工程师定位需求中潜在的错误。4)为了提升本文中性质验证可处理的问题规模,采用了符号执行进行了优化。

关键词： 智能合约   隐私保护   形式化方法   并行随机多角色博弈  

摘要： 随着新兴的区块链技术的出现,智能合约正面临着极大的安全隐患。仅2019年上半年就有24%的区块链用户遭遇过隐私数据泄露事件,隐私数据保护问题日益成为人们关注的焦点。随着区块链用户数量的不断增加,隐私数据泄露的问题也愈发严重。在使用智能合约的过程中,姓名、住址、电话号码和出生日期等个人隐私数据不经意间被智能合约收集,在缺乏对其保护的情况下容易发生泄露问题,给个人隐私安全带来隐患。本文主要针对当前智能合约存在的内部隐私数据安全性不足以及外部访问保密性不足的问题,给出了相应的解决方案:(1)本文提出了一种基于随机模型检验的智能合约隐私保护框架。将智能合约用承诺元组进行描述后建模为一个离散时间马尔可夫链模型。将智能合约中隐私数据根据其敏感度属性定义敏感度元组,并且设计出一套带有敏感度的隐私规约模板。最后选择现存的一个电子商务智能合约进行实例研究,分析此智能合约中是否存在逻辑错误而产生的隐私泄露情况以及查找该智能合约中最可能发生隐私数据泄露的调用方式,从而加强智能合约存在的内部安全性保护。(2)本文提出一种基于博弈理论的智能合约隐私保护框架。将访问者与被访问合约作为博弈的双方,建立并行随机多角色博弈模型。该模型从收益和代价两个角度出发,计算双方最大收益值作为模型博弈的结果,并且验证此模型是否成功阻止恶意访问者通过访问的性质,进一步改进智能合约隐私安全的不足,实现对智能合约的外部安全的隐私保护。

关键词： 形式化方法   需求建模   需求确认与验证  

摘要： 随着大量软件在工业界的广泛应用,越来越多的嵌入式系统的核心控制软件逐渐走向数字化控制的道路。随着计算机硬件性能的逐渐提升,人们期待用计算机去解决的问题越来越困难,这也导致现代工业控制软件日益庞大与复杂。在这种情况下,如何在安全攸关系统中保障系统的安全性显得愈加重要。工业界和学术界都认为对软件开发的起始点对系统需求进行形式化分析与验证是保障嵌入式系统软件可靠性的一个重要手段,然而,如何在工业界的大型软件项目中应用形式化方法仍然是一个亟待解决的难题。工程师在生产实践中应用形式化方法时,仍缺少自动化的工程性方法来高效地选择和建立更加精准的需求模型与性质,且缺少严谨的方法论去确认和验证所建立的需求模型。为了解决上述问题,本文针对形式化方法在工业界中的应用进行了研究和探索,其主要的研究内容和贡献如下:·设计了一个领域专用的轻量级需求建模语言AASRDL在特定嵌入式领域中,通用的建模语言学习曲线陡峭,学习成本巨大,无法满足工程师快速建模的需求,为了解决这一难题,通过总结相应的嵌入式领域特征,本文设计了一个轻量级领域专用的需求建模语言AASRDL,用于需求规约的快速构建。同时,本文还提供了一个模板来引导构建形式化需求模型;·提出了一种基于NLP的需求规约自动生成方法为了解决工程师难以熟练使用形式化语言描述待验证的安全性质问题,提出了一个可以将自然语言描述的性质转化为需求规约的方法。通过分析安全需求的性质描述特征,提出了一个安全需求的语义模型,使用句法切块技术和依存关系分析技术进行安全需求中的信息抽取并将其存储在语义模型中,并最终根据目标语言翻译成相对应的需求规约;·提出了一个系统性工程方法FREPA提出了一个系统性的可以指导工业界在嵌入式领域中进行形式化需求建模和确认验证的方法FREPA;该系统性的方法主要包括在嵌入式系统中如航空航天系统进行系统需求模型的构建、确认和验证操作,主要分析技术包括基于图标的需求审查、模型模拟执行、基于MC/DC覆盖准则的测试用例自动生成、性质验证;·支撑工具及其应用本文开发了基于FREPA方法的支撑工具,该工具可以实现需求建模和确认验证的自动化操作,并在相应的实际项目中进行了实验和验证。目前为止,本文所提出的方法已经成功地被应用于七个航天飞行器和两个航空发动机控制系统的软件开发过程中。实验表明本文的方法论及其支撑工具工具能够在实际项目中进行有效的形式化建模和确认验证。

关键词： 初中物理   单元设计   知识结构化   浮力  

摘要： 在初中物理课堂教学转型中，注重单元教学的整体设计是很重要的。教师通过单元设计能帮助学生更加系统地梳理知识点，实现知识结构化，并且能指引学生树立“大概念”思维，这对于学生的知识获取有极大帮助。对此，文章结合苏教版八年级下册第十章“压强与浮力”单元，对初中物理单元设计路径进行全面分析。

关键词： 5GEAP-TLS协议   OWE协议   形式化方法   符号模型   Dolev-Yao模型  

摘要： 目前,移动通信网络和无线局域网已经成为生活中必不可少的一部分。为了保障移动通信网络和无线局域网的安全性,研究人员设计了各种身份认证协议以确保合法用户的安全接入。然而,很多身份认证协议在投入使用多年后仍被发现存在重大安全漏洞。因此,针对身份认证协议的安全性分析至关重要。最近,一些研究人员采用形式化方法对5G网络和无线局域网中的身份认证协议进行安全性分析。但是,这些工作在形式化建模协议交互细节、攻击者能力以及安全目标时存在不同程度的简化,可能会导致协议潜在的安全隐患无法被发现。本文使用形式化方法中的符号模型对5G网络中的5G EAP-TLS协议和无线局域网中的OWE协议进行安全性分析,构建了多种模式下的协议交互模型,设计了不同场景下的攻击者模型和多种安全目标,对于安全目标无法满足的情况,分析了协议潜在的安全隐患并提出了相应的防护建议或修订方案。本文的主要工作如下:1.针对5G网络,本文提出了一种面向5G EAP-TLS协议的细粒度形式化分析方案。该方案以TS 33.501标准为依据,根据标准文档中描述的协议交互流程还原了协议参与方之间的交互细节。相比于现有工作仅构建了 RSA密钥协商模式下的协议交互模型,本文还构建了 Diffie-Hellman密钥协商模式下的协议交互模型,同时根据标准文档还原了协议的四个参与方。此外,本文还分析了 5G EAP-TLS协议面临的安全威胁,扩展了 Dolev-Yao攻击者模型的攻击能力,提出了多种运行场景下的定制攻击者模型。本文还定义了协议运行过程中应该满足的安全目标。与现有工作相比,本文不仅定义了保密性和认证性,还定义了前向保密性和隐私性。2.针对无线局域网,本文提出了一种面向OWE协议的细粒度形式化分析方案。该方案以802.11标准为依据,还原了协议的三个运行阶段以及协议交互过程中使用的计数器机制。为了更细粒度地还原协议交互细节,本文构建了PMK缓存模式和常规模式两种模式下的协议交互模型。此外,本文还考虑了恶意参与方参与协议的运行场景,提出了多种运行场景下的定制攻击者模型。本文在标准文档缺乏对OWE协议安全目标明确定义的情况下,分析了 OWE协议的安全需求,定义了协议在运行过程中应该满足的保密性和前向保密性。3.本文分析了 5G EAP-TLS协议和OWE协议潜在的安全隐患并提出了相应的防护建议或修订方案。本文使用形式化验证工具SmartVerif验证了5G EAP-TLS协议和OWE协议的协议交互模型、攻击者模型和安全目标。实验结果表明,在一些特定攻击者场景下,5G EAP-TLS协议和OWE协议的部分安全目标遭到破坏。针对安全目标遭到破坏的情况,本文总结了 5G EAP-TLS协议的4类安全隐患和OWE协议的3类安全隐患并提出了防护建议或修订方案。对于修订后的协议本文使用验证工具再次验证,实验结果表明修订后的协议满足了本文定义的安全目标。

关键词： 离散事件系统   自动机   隐蔽性   网络空间安全   形式化方法  

摘要： 随着计算机和网络不断融入到我们生活中,网络安全问题越来越受到人们的重视。从居民个人身份信息的保护到国家网络安全的维护需求一直在推动着网络空间安全相关问题的研究。安全形式化方法作为研究网络空间安全的工具之一,持续受到人们的关注。隐蔽性是一个重要的网络安全属性,它指系统的敏感信息是否可以被外部观察者(如入侵者)所推知。在离散事件系统中,隐蔽性概念主要包括当前状态隐蔽性、语言隐蔽性、初始状态隐蔽性、初始-末端状态隐蔽性、K步隐蔽性和无限步隐蔽性等。当一个离散事件系统被证实是非隐蔽时,各种方法被提出用来综合保证系统的隐蔽性,如监督控制策略,动态模板策略和混淆策略等。其中混淆策略主要通过插入函数或编辑函数对系统的输出行为进行修改以保护系统的秘密语言。本文的主要研究成果如下:1.本文首先研究了基于公有插入函数的当前状态隐蔽性隐蔽性强制执行综合问题,提出了综合公有插入函数方法。这种方法是基于修订后的可执行性定义以及改进的贪婪准则而设计的。本文提出的算法是可行并且完备的,可用于完全解决公有插入函数的综合问题。此外,本文提出的程序算法简化了私有执行插入函数的设计步骤并证明在某些特殊情况下可以在低计算复杂度下综合私有强制执行插入函数(或公有强制执行插入函数)。2.本文又研究了基于插入函数的无限步隐蔽性和K步隐蔽性综合强制执行问题。我们首先审视了现有的插入机制,并从纯自动机的角度来理解插入机制,然后建立两个新的自动机来分别识别无限步隐蔽性安全语言和K步隐蔽性安全语言。最后将插入机制应用到强制执行无限步隐蔽性和K步隐蔽性。相应的,本文也对计算复杂度进行了讨论。本方将插入函数的强制执行从当前状态隐蔽性推广到无限步隐蔽性和K步隐蔽性上来。3.本文还研究了基于属性编辑函数的隐蔽性强制执行问题。在我们所提出的编辑机制中,编辑函数在满足替换函数给出的替换规则下执行插入或替换操作来修改系统的输出行为。此外,只有满足预期接收者身份属性的外部观察者才能够基于插入或者替换区分符号,并根据替换函数来恢复未编辑的原始输出序列。4.在对无限步隐蔽性的强制执行研究中发现,对无限步隐蔽性中不安全语言识别方法的改进也可以应用到随机离散事件系统中的几乎无限步隐蔽性验证中去,从而使几乎无限步隐蔽性的验证计算复杂度得到降低。

关键词： 形式化方法   形式化验证   故障检测   蕴含关系   误差推理  

摘要： 随着形式化验证技术的应用与发展,定理证明和模型检测两种验证技术优势互补,在安全攸关系统(航空工业、探月工程、自动驾驶技术等)的验证上,发挥了越来越重要的作用。定理证明技术用演绎推理手段,对系统是否满足特定的安全性质进行严格的数学推导证明,已有多种基于定理证明的验证工具问世。然而,误差在系统中是普遍存在的,目前大部分基于定理证明的验证理论较少考虑系统中的误差参数。因此,针对含误差的安全攸关系统的形式化验证工作有重大的理论及现实意义。另一方面,多项式代数系统在描述连续数据交换、连续状态等方面有较强的刻画能力,此外近年来,多项式代数(符号计算的分支领域)也有长足的发展。例如:实根隔离算法、Gr(?)bner基、吴方法、半代数系统求解。正是基于以上思考,以及结合几年来在这一领域的持续研究,我们在以下几方面有所创新:(1)误差线性断言推理方法:证明了误差线性断言零点集为凸集,提出了求解误差线性断言顶点集的方法,并证明了该方法的正确性。经分析相关概念及定理,将判断误差线性断言之间的蕴含关系转化为前驱断言的顶点是否被包含在后驱断言的零点集的判断问题,从而给出了判断误差线性断言的蕴含关系的方法步骤。最后,将该方法应用在火车匀速和加速运动上,并用大量随机误差参数模拟验证了该方法的有效性。(2)非线性误差多项式断言推理方法:将误差多项式断言之间的蕴涵关系转化为它们零集之间的包含关系;将误差多项式断言转换为一阶多项式逻辑公式。研究结合基于柱形代数分解的量词消去方法,将误差多项式断言零点集之间的包含关系转化为特定一阶多项式逻辑上的量词消去问题。最后,以目标拦截问题的为例,通过大量随机误差参数验证了该方法的正确性。(3)结合误差概率信息的误差多项式断言推理方法:用截断正态区间来描述误差,部分地简化了截断正态区间的运算,提出了与误差的概率信息相结合的误差多项式推理方法。依据误差的统计学信息,我们的方法能更及时地判断出系统潜在的非误差故障。最后给出该方法在火车加速动力分配两体问题上的应用,经对其误差参数的大量测试,测试结果与理论推理结果一致。(4)在误差语义上,用区间和截断正态区间来刻画误差,分析了区间运算中存在的两个问题(不可逆性、范围扩大性)。本文推理方法(误差线性断言和非线性误差多项式推理方法、结合误差概率信息的推理方法)大大的避免了这两种问题。误差多项式断言是多项式代数断言的推广,当区间数的上界和下界相等时,误差多项式断言就退化为经典多项式断言,因此我们提出的误差多项式断言与经典多项式断言逻辑自洽。定义了误差多项式断言的零点集,并且同样做到了与经典多项式零点集自洽,并给出了误差多项式断言蕴含关系的等价条件。

关键词： 形式化方法   混合代码验证   模型检测   自动验证  

摘要： 随着软件工程技术的不断发展,软件的功能变得越来越丰富,这给人们的生活带来了极大的便利性,但软件的复杂性和多样性,也使得软件安全漏洞与日俱增,传统的软件测试方法说明软件存在某些安全漏洞,但是不能保证软件不存在某类安全漏洞,相比之下形式化验证方法则可以做到这一点。操作系统作为基础系统软件,其安全性至关重要,使用形式化验证方法对操作系统内核的实现代码进行验证,是保证其安全性和正确性的有效手段。而操作系统的内核实现代码多为C与汇编的混合代码,如果使用传统的形式化验证方法进行验证,存在人工参与度高、验证效率低、验证复杂度高等问题,因此本文主要以混合代码的自动形式化验证为研究背景,重点研究了混合代码自动形式化验证技术与实现方法。本文主要工作如下:(1)基于模型检测技术,提出了一种面向汇编代码的自动形式化验证方法。为了提高验证效率,降低验证工作量,构建了ARM汇编指令模型库,该模型库为ARM汇编代码的建模与验证提供了统一的接口,利用该模型库可以方便地对汇编代码进行抽象建模和验证。(2)针对混合代码中C代码与汇编代码嵌套调用带来的建模困难和验证复杂度高等问题,提出了一种混合代码的建模与验证方法,通过对混合代码中的C代码进行编译和抽象建模,使得可以在统一的抽象级别对C语言和汇编语言代码进行验证,大大提高了验证效率。在混合代码验证方法中还加入了对中断处理程序的验证支持,并使用了中断执行预测算法对由此产生的模型状态爆炸问题进行了解决。(3)为了进一步提高混合代码验证的自动化程度,基于本文提出的混合代码自动形式化验证方法开发了一个混合代码自动形式化验证工具,该工具提供了C代码功能性验证、自动解析混合代码生成抽象模型、基于模型检测的安全属性验证等功能,利用该工具对μC/OS-II操作系统中的混合代码函数进行了验证,展示了工具使用的便利性以及验证方法的有效性。