教学课程资源库 更多>>

关键词： 飞机   结构设计   数字化   设计体系  

摘要： 近年来随着数字化设计技术的不断发展、推进,飞机结构设计与数字化设计技术的结合应用也成为重要的发展趋势。以飞机结构中的数字化设计体系为重要依托,推进飞机结构设计的完善、推动其性能提升也成为数字化设计体系应用的重要目标。本文就飞机结构设计中的数字化设计体系的应用为主要研究对象,针对其设计方法以及具体实践等展开分析。

关键词： UML   建模   智能公交调度实训系统  

摘要： 实践教学是人才培养的重要环节,也是提高教学质量和教学效果的重要手段。为了在实践性教学、培训手段及科研上有重大突破,本文以公交调度指挥系统中的重要岗位--车站调度员为研究对象,利用UML对智能公交调度教学实训系统进行建模。对公交调度指挥工作进行分析,运用UML建立可程序化的调度指挥模拟仿真体系结构;对车站技术作业过程进行分析,运用UML建模技术和仿真技术建立作业控制系统仿真模型,使车站技术作业过程仿真效果具有真实可信性。

关键词： Coq   矩阵   形式化验证   定理证明   记录类型  

摘要： 矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制。Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂。针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质。基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证。同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便。

关键词： 形式化验证   形式化方法   软件   计算系统   硬件系统   自动机理论   逻辑演算   形式语言  

摘要： 形式化方法是建立在逻辑演算、形式语言、自动机理论、程序语义、类型系统等理论基础之上,对计算系统进行描述和分析的一系列符号与技术的集合。形式化方法可指导软/硬件系统的规约、设计和验证,是改善和确保计算系统质量的重要方法。历史上,形式化方法在硬件和协议验证方面取得巨大成功。

关键词： 用电信息采集   通信协议   一致性测试  

摘要： 基于面向对象思维建模设计的新一代用电信息采集通信协议,对它所使用的范围是比较大的,而且在配置方面具有很好的灵活性,具有各种不同形式的服务方法。为了能够让通信协议的各方面的优势得到充分的发挥,此次文章对面向对象的用电信息采集通信协议进行了分析和研究,并且对测试用例进行了相应的设计,可以进行协议一致性测试。

关键词： Airlight   area efficiency   dehazed images   energy efficiency   hardware architecture   transmission rate  

摘要： The function of an image dehazing algorithm restores a hazy image back to a clear one. This technique can be equipped in Advanced Driver Assistance Systems (ADAS) to further improve driving safety. Advanced display resolutions and high frame rates are critical to improve the reliability of ADAS. However, they cause a serious limitation on the hardware realization of an image dehazing algorithm. In this paper, an algorithm and architecture design of a hardware-efficient image dehazing engine are proposed. This dehazing algorithm comprises two core techniques: a low-complexity airlight estimation (LAE) and an independent transmission rate estimation (ITRE). LAE can efficiently predict the airlight without massive sorting processes and a computationally intensive filtering. Moreover, in its hardware architecture, a preluded airlight estimation is proposed to yield an efficient data scheduling. Being independent of the airlight, ITRE is able to solely predict transmission rates. This enables LAE and ITRE to be concurrently processed, improving the throughput of their hardware architectures. Compared with other sophisticated studies, this study demonstrates a competitive performance in peak signal-to-noise ratio, structural similarity, contrast distortion, and computational efficiency. The hardware architecture is realized using Taiwan Semiconductor Manufacturing Company CMOS 0.18-mu m technology, and logic gate count is 32.6 K. Its working frequency is 200 MHz with a power consumption of 16.5 mW. The maximum throughput is as high as 600 megapixels/s, which can support 4 096x2 160 at 60 frames/s. The experimental results indicate that this paper demonstrates superior energy and area efficiencies.

关键词： APFD Metric   K-Means Clustering   Object Oriented Programming   Regression Testing   Test Case Prioritization  

摘要： In the software maintenance activity, regression testing is performed for validing modified source code. Regression testing ensures that the modified code would not affect the earlier tested program. Due to a constraint of resources and time, regression testing is a time-consuming process and it is a very expensive activity. During the regression testing, a set of the test case and the existing test cases are reused. To minimize the cost of regression testing, the researchers proposed a test case prioritization based on clustering techniques. In recent years, research on regression testing has made significant progress for object-oriented software. The empirical results show the importance of K-mean clustering algorithm used to achieve an effective result. They found from experimental results that their proposed approach achieves the highest faults detected value than others.

关键词： AdBlue urea   Ammonia   DeNO(x)   Liquid-phase decomposition   Selective catalytic reduction  

摘要： Difficulties in decomposing AdBlue to ammonia limit the applicability of selective catalytic reduction systems at low exhaust temperatures. Investigations on the decomposition of AdBlue in the liquid phase under elevated pressure at temperatures up to 165 degrees C were carried out. Besides effects of inorganic catalysts, the impact of pH on urea decomposition was examined. After dissolution in aqueous phase, the compounds ZnO, WO3, and MoO3 were found to be effective in liquid-phase AdBlue decomposition. However, the efficiency was dropping significantly over few hours. Decomposition of AdBlue urea was also found to be favored for alkaline and acidic conditions.

关键词： Formal methods   formal verification   IEC 61131   IEC 61499   industrial automation systems (IAS)   industrial control  

摘要： Industrial automation systems (IAS) need to be highly dependable;they should not merely function as expected but also do so in a reliable, safe, and secure manner. Formal methods are mathematical techniques that can greatly aid in developing dependable systems and can be used across all phases of the system development life cycle (SDLC), including requirements engineering, system design and implementation, verification and validation (testing), maintenance, and even documentation. This state-of-theart survey reports existing formal approaches for creating more dependable IAS, focusing on static formal methods that are used before a system is completely implemented. We categorize surveyed works based on the phases of the SDLC, allowing us to identify research gaps and promising future directions for each phase.

关键词： 校企合作   软件工程   教学改革  

摘要： 软件工程是软件工程专业的一门专业基础课,传统的理论教学容易流于形式,空洞说教,学生的学习积极性不高。校企合作在《软件工程》课程中的应用,充分考虑当今最先进技术的发展趋势,共同规划和开发出软件工程课程配套的教学大纲、多媒体课件、教案和试题库等教学资源,为软件工程课程提供充分的资源保障。根据企业对学生的最新需求,以企业的真实项目为依托,通过不同小组完成不同的案例使学生掌握软件工程课程的相关知识和技术,为学生更深入的学习和就业打下扎实的基础。