教学课程资源库 更多>>

关键词： Robotic systems   Task specific knowledge  

摘要： Robotic systems that are capable of learning from experience have recently become more common place. These systems have demonstrated success in learning difficult control tasks. However, as tasks become more complex and the number of options to reason about becomes greater, there is an increasing need to be able to specify the desired behavior in a structured and interpretable fashion, guarantee system safety, conveniently integrate task specific knowledge with more general knowledge about the world and generate new skills from learned ones without additional exploration. This thesis addresses these problems specifically in the case of reinforcement learning (RL) by using techniques from formal methods. Experience and prior knowledge shape the way humans make decisions when asked to perform complex tasks. Conversely, robots have had difficulty incorporating a rich set of prior knowledge when solving complex planning and control problems. In RL, the reward offers an avenue for incorporating prior knowledge. However, incorporating such knowledge is not always straightforward using standard reward engineering techniques. This thesis presents a formal specification language that can combine a base of general knowledge with task specifications to generate richer task descriptions. For example, to make a hotdog at the task level, one needs to grab a sausage, grill it, place the cooked sausage in a bun, apply ketchup, and serve. Prior knowledge about the context of the task, e.g., sausages can be damaged if squeezed too hard, should also be taken into account. Interpretability in RL rewards - easily understanding what the reward function represents and knowing how to improve it - is a key component in understanding the behavior of an RL agent. This property is often missing in reward engineering techniques, which makes it difficult to understand exactly what the implications of the reward function are when tasks become complex. Interpretability of the reward allows for bet

关键词： 统一建模语言UML   线上教学   教学设计   教学特色  

摘要： 新冠肺炎疫情防控期间,《统一建模语言UML》课程首次采用了线上教学的模式.本文主要从课程目标、教学平台、教学资源、教学策略、课程评价五个方面介绍了UML线上教学的课程设计方案,并简要说明了教学特色以及所达到的教学效果.

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

摘要： 近几年来,我国的国民经济发展速度非常迅速,也在一定程度上促进了道路桥梁的发展和壮大.由于工程建设规模的不断扩大,进行施工时会存在很多较为复杂的施工工艺,这也就要求了道路桥梁工程需要进行合理的结构化设计.通常情况下的结构化设计的特点是具有连续性.最为主要的就是要按照该项目的整体来对桥梁的承载能力进行分析.同时还要利用科学的手法来确定每个结构所能承受的范围,进而在一定程度上减轻运送的内力,节约成本根据工作实践经验对结构化设计在道路桥梁设计中的运用进行了分析和探讨.

关键词： 小学数学   结构化设计   深度化教学  

摘要： 小学数学教学中教师应认识到深度教学的重要意义,帮助学生深刻地理解数学知识的本质,使其能够真正地灵活应用,为学生更好地掌握所学知识,学习更深层次的数学知识奠定基础。为获得预期的深度化教学目标,应认真研究小学数学各知识点,把握各知识点之间的内在关联,做好结构化设计,使各知识点在学生头脑中留下深刻印象,为深度化教学任务的顺利完成奠定坚实的基础。

ISBN: (纸本)9787517084617

关键词： 实践能力   软件工程   教学模式  

摘要： 在科技产业迅速发展的背景下,培养软件人才的实践能力具有重要意义。本文在研究和分析软件工程课程教学现状的基础上,探索了基于实践能力培养的软件工程课程教学模式,结合以成果为导向的教育理念,重新改进课程教学内容,完善软件工程课程体系,采用多元化课程教学方法,注重提升学生工程实践能力,进而持续提高人才培养质量。

关键词： 手机营业厅   客户端   移动业务   结构化设计  

摘要： 近年来,移动通信市场快速发展,各类业务及多样化的服务手段相继推出,整体市场竞争形势更加激烈。尤其客户在实体营业厅等候时间过长的问题还未解决问题更加突出,线下实体营业厅和电脑端网上营业厅均无法满足客户随时随地查询办理业务的需求。随着智能手机的快速增长,为有效缓解实体营业厅和网上营业厅的客流压力、减少运营成本、顺应整个市场的竞争形势,同时进一步提升用户的粘性、满意度,掌上营业厅客户端作为有效的解决难题手段而出现,并以“方便、优惠、贴心”的服务方式,让客户感受“足不出户24小时随时办理业务”的全新体验,从而满足用户对服务的全方位便捷要求。本文以中国移动河南公司作为研究对象,阐述了河南移动掌上营业厅客户端的需求分析与业务实现,其中包含大量业务流程分析、系统接口分析、数据库表等内容,目前已在线上运营,系统情况运行稳定,满足河南移动客户发展需求。

摘要： 十九届四中全会以来,习近平总书记在不同场合多次强调:推进国家治理体系和治理能力现代化建设,其重要论述包括"要以信息化推进国家治理体系和治理能力现代化,……更好用信息化手段感知社会态势、畅通沟通渠道、辅助科学决策。"在此背景下,近年来,我国软件和信息技术服务业市场规模保持较快增长,2018年仅电子政务市场规模就约为3134亿元,同比增长15.1%。据工信部最新数据统计显示:2019年,我国软件业完成软件业务收入71768亿元,同比增长15.4%,利润总额9362亿元,同比增长9.9%。2019年全国软件业综合发展指数为

关键词： 有限域   多项式运算   形式化方法   定理证明   Coq   加密   形式化验证  

摘要： 有限域GF（2~n）是多种安全关键性算法的基础,它在AES加密算法,椭圆曲线加密,感染函数掩码等领域有重要作用。有限域上的运算因为自身的复杂性而容易出错,这些错误容易导致系统产生问题。基于测试和基于模型检测的验证方法只能在n固定的特定有限域上进行验证,当n很大时,很难取得有效而全面的验证。基于交互式定理证明器的形式化验证为有限域性质的通用验证提供了可能性,而这有助于有限域上运算的验证,但这方面的工作难度比较大。基于定理证明的验证方法的工作过程和数学定理的证明过程类似,首先需要建立一组定义并证明一批引理,之后在这些前置工作的基础证明最终目标,因此首先需要完成相应的数学理论在定理证明器中的形式化,构建相应的形式化的数学理论库。本文的主要目标是建立在对有限域GF（2~n）的一个形式化数学库,包括对有限域相关概念进行构造性定义,并在构造性定义的基础上对域的一些性质进行形式化验证。针对这些问题,本文借助定理证明器Coq,对有限域GF（2~n）上元素及其基本运算进行了形式化定义,并且对一组同有限域有关的基本性质进行了形式化验证,包括有限域加法基本性质验证、有限域乘法部分性质的验证。这项工作为有限域的完整的形式化,以及基于有限域的算法的形式化验证打下了一个基础。本文考虑了多种方法来实现对有限域进行形式化验证,主要的研究成果如下:第一,本文完成了一个特殊的有限域GF（2～8）的形式化定义,并在此基础上进行了完整的形式化验证。这个有限域主要用于AES算法,是AES算法形式化验证中的一个难点。之后本文将所验证的性质进行了扩展,并以此完成了AES算法的形式化验证中有难的列混淆部分的验证。第二,针对前面工作只针对某一特定有限域展开的局限性,本文以一种归纳结构作为有限域GF（2 ~n）上元素的载体,以递归为主要手段在完成了有限域GF（2~n）上运算的形式化定义。这种方式完成的定义适用于任意大小任意结构的有限域GF（2~n）。第三,本文对有限域GF（2~n）的相关性质进行了形式化验证。在加法方面,完成了对加法交换律,结合律,单位元,逆元等基本性质的形式化验证。乘法方面,由于直接验证很困难,本文分成了几个部分来做。目前完成了构成有限域GF（2~n）乘法的多项式乘法相关性质和取模运算部分性质的形式化验证。并在此基础上完成了有限域乘法部分性质的形式化验证。本文主要通过归纳的方法进行验证,验证的性质适用于任意大小任意结构的有限域GF（2~n）。本文研究所形成的形式化数学库也可以为其它研究提供帮助。

关键词： 安全苛求系统   道岔状态监测单元   系统开发   Stateflow   形式化验证   仿真  

摘要： 论文以道岔状态监测单元作为研究对象,针对智能化情景下的铁路系统安全决策问题,使用形式化开发方法严格的定义了该系统软件的逻辑决策层,完成了系统原型机的构建与软件决策进程的验证,增强了系统的可信性。基于安全苛求系统的特征构建系统硬件架构,基于系统的可验证性要求,设计系统软件架构。在系统软件架构中将控制流与数据流分离,作为系统软件的逻辑决策层和形式化建模和验证的对象。并结合实际应用场景提出保障系统可靠性的措施;使用工具链建立从半形式化到形式化的建模验证方案。针对系统软件的逻辑决策层,借助基于系统理论的事故模型过程分析方法(STAMP)的危险致因分析来发现当前系统的缺陷并反推系统的安全约束,并根据实际的应用场景完善功能需求,结合软件决策层的层次结构建立需求元模型。根据需求元模型确定参数类型和程序框架,建立数据字典,并一步实例化元模型中的功能,建立程序流程图。最终将数据参数与程序流程图模型化为Simulink的Stateflow模型,为形式化建模提供实现的模板和仿真依据;形式化建模和验证阶段根据系统软件逻辑决策层纯布尔逻辑的特性定制B方法的建模和验证方案,使之更简单、高效,且有针对性;根据元模型和Simulink的Stateflow模型形式化建模,并使用安全约束构建的不变式和Pro B的模型检测功能证明模型的正确性,最终生成目标代码。最后,添加并集成具体的实现算法、构建联锁环境,在仿真环境中进一步测试和确认系统的功能满足性。论文中实现了道岔状态监测单元软件逻辑决策层的形式化开发。该安全关键模块的逻辑模型在Atelier B平台中被证明通过,并可生成相应的嵌入式代码,将代码集成并在仿真环境中完成了仿真。课题的整个技术过程证明了课题中设计的开发路线适用于定义和开发此类复杂逻辑系统,可为安全苛求系统的开发提供参考。