教学课程资源库 更多>>

关键词： 财务共享服务   UML建模   财务系统   Spring技术  

摘要： 财务共享服务中心作为新型的财务管理模式,采用标准化、流程化管理来展开财务管理工作,搭建了集中、高效、统一的信息化平台,能够对企业生存、市场、财务、物流、客户等进行全方位管理。目前某保险集团股份有限公司采取分散的财务管理模式,导致在财务报账、审批、统计等方面难以协调一致,财务管理工作效率低下,财务数据难以及时统计汇总,形成独立的信息孤岛,导致存在一定财务风险。本文再造财务业务流程,构建财务共享服务中心,同时设计开发财务系统,实现对财务工作的集中高效管理。通过对保险公司财务系统的建设,首先,阐述了研究背景和集团企业财务管理面临的困难,提出构建信息化系统来管理财务数据,对国内外研究情况进行分析,指出了研究给社会带来的应用价值。然后对财务共享服务的相关概念、特征以及运营模式等进行阐述,对财务共享服务的集团公司实施过程和运营保障进行分析,对系统使用技术进行的分析,介绍了Spring、Struts2、Hibernate核心技术的特点、工作原理以及框架构成。再次,探讨了系统建设的必要性,指出了财务管理的业务流程,分析了系统功能用例和构成,明确了预算、付款、结算、合同等管理对象,并从性能、安全性、扩展性等方面介绍了非功能性需求。文章重点从总体上设计了财务系统构成,从多层次多方面设计了系统应用架构、逻辑结构、系统组成及部署架构、采用的关键技术,采用时序图、流程图、数据库E-R等UML建模形式详细设计了软件功能。最后,描述了系统开发软件环境搭建情况,通过编码实现了系统功能,展示了界面内容和核心程序代码,确定了系统处理流程和管理内容。对系统主要业务进行了测试和验证。配置了测试环境,设计不同类型测试的测试用例,采用测试工具完成数据、功能、性能等方面测试,验证系统能够满足用户使用需要。本文通过对财务共享服务中心的研究,构建了财务管理系统,统一了业务流程,转变了服务方式,有效提高了公司运营效率和服务质量,节约了管理成本,促进了企业市场竞争力的提升。

关键词： 机器视觉   软件工程   智能化教学  

摘要： 基于我国工业智能软件地位作用进一步提高,但企业在工业软件应用上竞争力还比较弱的产业现状,以基于机器视觉的在线检测技术的应用实践为例,探讨面向智能化应用的软件工程人才培养模式,丰富软件工程专业教学实践,拓展软件工程人才的就业方向。

关键词： 神经网络加速器   体系结构设计   分解算法   Winograd算法   高性能运算   并行运算   MTCA算法  

摘要： 随着卷积神经网络在多领域得到广泛应用,各种平台和设备对神经网络的需求日益突出。由于神经网络具有高吞吐、高计算的特性,通过提升卷积神经网络硬件加速器的计算效能、硬件利用率和灵活性来获得更好地加速效果显得尤为重要。本文围绕不同类型的卷积运算加速器的算法加速及硬件体系结构展开研究,主要工作如下:本文基于脉动阵列结构提出一种动态可重构的通用卷积神经网络加速器设计方案,与传统的加速器设计不同,该加速器在同一硬件架构的基础上实现了对标准卷积、分组卷积和深度可分离卷积的加速计算,具有高度的适用性和灵活性。本文针对大规模尺寸的卷积层运算,提出一种基于MTCA分块并行计算的方法,实现了卷积展开和中间过程矩阵的分块,有利于硬件上实现高度并行化。在此基础上,提出了中间过程矩阵最优分块的具体计算方法,实现了算法的最优,较传统的im2col算法节省了60%以上硬件存储空间,尤其是在计算较大尺寸卷积情况下,较传统im2col算法节省近82%的存储空间,为大尺寸卷积计算提供了有效的解决方案。本文针对具备稀疏特性的卷积层运算,提出一种卷积基于SparseWinograd F(2×2,3×3)分解计算方法,不仅消除了Winograd算法复杂的预运算,降低了算法硬件实现难度,同时也极大拓展了硬件的灵活性。对于VGG-16、Mobile Net V1实现了3倍至4.15倍的加速,较Winograd算法提升了1.4-1.8倍左右的加速。本文基于SCALE-SIM模拟器以轻量级网络Mobile Net系列作为测试基准,在不同实验条件下加速器对新型卷积运算加速进行了详细的实验分析。通过系统全面的实验,我们为基于脉动阵列的轻量级神经网络加速器的设计空间,主要对包括运算效率、加速比、循环时间等各指标权衡在内进行了深入探索,解决了在该领域研究成果不足的问题,为后续的开发人员更快、更好的开发针对轻量级神经网络的硬件加速器提供了极大的便利。通过我们的研究实现了Mobile Net V1在特定数据流和核心计算规模下近1.2倍的加速。

关键词： 理论计算机科学   形式化方法  

摘要： 理论计算机科学是整个计算机科学的理论根基。自从Alonzo Church和Alan Turing分别使用形式语言与自动机来为人类的计算行为进行理论建模开始,理论计算机科学领域的学者们就将计算本身作为一种客观存在,以"格物,致知"的态度来探究计算的本质原理。现代计算机科学与技术及其相应工程与应用的蓬勃发展,为这一基础学科提供了创新的舞台,使其充满了活力。传统上,理论计算机科学因所使用的数学语言与理论工具的不同,被分为两大分支:一类专注于对算法和计算复杂性的研究,而另一类则关注程序语言以及形式化方法。前者往往使用组合数学、概率、分析等更加具体的数学工具,研究计算问题的算法上界或者计算复杂性下界;而后者则更多地使用逻辑、代数、范畴论等抽象的数学工具,为计算建立抽象模型,探索抽象模型

关键词： Redis集群   分布式系统   形式化方法   CSP   一致性  

摘要： 随着大数据时代的到来,传统数据库已难以满足高并发情况下的数据访问,Redis内存数据库因能为大数据提供高性能和稳定性而广为采用。Redis不仅支持多种类型的数据结构、事务功能、订阅发布机制,还具有故障自动处理等特性。随着应用中数据量的增长,Redis集群解决了服务器负载量大以及单机下的内存瓶颈等问题。然而随着Redis集群方案被广泛使用,也出现了故障转移后数据同步低效、负载均衡优化等问题,为保证Redis集群的高性能以及高可用,需要从形式化方面对Redis集群进行建模分析与研究。本文的研究对象是Redis集群消息通信机制,其目的是实现集群的一致性与可用性。基于形式化方法的高可信特性和Redis集群一致性和可用性的需求,采用通信顺序进程(Communicating Sequential Processes,CSP)对Redis集群消息通信机制进行形式化分析与验证。通过分析消息通信各个实体之间的行为,将整个系统抽象为Meet消息通信和Ping-Pong消息通信两个模块,并给出了相关集合、消息和通道的定义,构建了Redis集群消息通信机制的CSP模型。然后,采用模型检测工具PAT(Process Analysis Toolkit)对构建的CSP模型进行代码实现,完成了常量、变量、通道的定义以及Meet消息通信和Ping-Pong消息通信过程的代码实现。接着对该模型需要验证的性质进行定义与实现并给出验证结果。由结果可知,Meet消息通信模块满足无死锁性和可交换性,即握手的两个节点能够实现消息交换。另外,Ping-Pong消息通信模块满足无死锁性、可结束性、可传播性和最终一致性,即任何一个节点的消息最终总能在集群中被其他节点获取。从形式化方法角度验证了Redis集群消息通信机制能够保证集群状态的最终一致性。最后,基于Redis集群消息通信机制引入了Redis集群故障处理机制,分析了复制、故障检测、故障转移三个过程并构建了Redis集群故障处理机制的CSP模型,接着验证了模型的命令可传播性、故障可测性和故障可转移性,从而保证了Redis集群的高可用性。随后,针对故障转移后数据同步的低效问题,通过引入父节点链的方式,提出一种将消耗网络带宽、计算资源的完全同步转换为高效率、低能耗的部分同步的优化方案,并通过形式化方法验证该方案的有效性。

关键词： 模型检验   安全性分析   增强飞行视景系统   形式化方法   安全性需求分配  

摘要： 增强飞行视景系统作为飞机上的复杂电子系统,传统的安全性分析面临工作量大,过于依赖分析人员经验,容易出错等问题,Petri网、概率模型等形式化方法虽然提高了分析的自动化水平,减少了一定的分析工作量,但也面临不能自上而下进行安全性需求分配的问题。为解决上述问题,提出了基于模型检验的形式化安全性分析方法。实现对增强飞行视景系统的定性、定量安全性分析,提高分析效率。研究包括以下几个方面:(1)首先,通过对该系统的架构和数据流进行抽象,分模块级、LRU级、系统级三层,建立了系统的形式化名义模型,并进行了验证。(2)研究模型扩展方法,编写故障库模板,将底层模块的故障模式注入到名义模型,建立形式化扩展模型。(3)将典型失效状态用形式化规约描述,进行自动计算,得到故障树最小割集,基于该最小割集进行了定性和定量分析,其中在定量分析,提出一种安全性分配方法,并实现了自动分配工具。结果表明,该方法自动化程度高,且解决了其它形式化方法如Petri网、概率模型等无法进行自上而下概率分配的问题,能够更加有效地促进系统设计阶段的安全性工作。

关键词： 新工科   软件工程   实践教学   教学模式  

摘要： 时代在不停地发展,教学模式也在不断地变革。新工科背景下,以提高人才培养质量为核心,衍生出各种各样新型的教学模式。本文对高校工程实践课程的教学模式进行研究和实践,包括课堂案例教学、网络非线性学习、校企合作、创新创业训练、商业项目实战等。

关键词： 状态机   单个对象   建模  

摘要： 状态机图是统一建模语言UML中的动态模型图,用来描述一个实体基于事件反应的动态行为.要研究某个实体或对象的单独的行为及状态变化,可以使用状态机模型图来表示.本文对状态机图进行了介绍,并通过实例进行状态机图的建模分析.

关键词： 类测试   扩展控制流图   面向路径   约束求解   测试用例生成  

摘要： 面向对象编程语言提供了继承、封装、多态的特性,提高了代码的重用性、安全性、维护性,给开发人员带来较大便利的同时,也给软件测试带来了一定的挑战。由于动态绑定和多态性,使得程序可执行的路径急剧增加,方法间、类间的关系变得更加复杂,给传统的类测试方法带了巨大的挑战,面向对象程序具有较高的复用率,更需要严格测试,避免错误的繁衍。针对上述问题,本文提出一种基于路径的类测试方法,围绕该模型本文做了以.下研究:(1)针对类的继承、多态特性引起的类间测试不充分问题,提出一种类成员方法扩展控制流图(Class Member Method Control Flow Graph,CMMCFG)结构。首先通过静态分析构建类的抽象表示模型,然后基于传统的控制流图进行节点替换和扩展,得到适用于面向对象程序的控制流结构。(2)针对由于类动态绑定特性而导致的可执行路径突增问题,提出面向类成员方法路径生成算法。通过将一条完整路径拆分成实例化子路径和基本子路径,采用路径组合的方式精简了路径数量,改善路径爆炸问题。(3)针对面向对象程序复杂路径约束提取和求解的问题,提出了面向路径的测试用例生成算法,采用符号执行技术完成成员方法路径分析,通过抽象内存建模精准提取路径上变量的语义和约束,并引入分支限界算法加快约束求解的速率。实验表明,本文提出的面向对象程序类测试方法有效的提高了类间测试的充分性,在一定程度上减少了不必要的路径选择,并为类成员方法自动生成有效的测试用例。

关键词： 形式化方法   事件逻辑理论   强认证性质   机密性   PUF双向认证协议  

摘要： 保证通信系统安全性的关键不仅取决于系统所使用密码算法的强度,而且还与使用的密码协议息息相关。在一些复杂的分布式网络环境中,如果密码协议无法提前预见所有可能的攻击很容易产生巨大的安全隐患,形式化方法就是证明密码协议安全性最有力的方法之一。事件逻辑隶属定理证明方法,是形式化方法的一种,基于消息自动机设计并对可能的协议动作都进行定义,通过分配给协议交互过程中的密钥,挑战数和消息不同的类型,为协议的操作提供新的证明规则和机制。本文使用事件逻辑理论对基于PUF的双向认证协议进行研究,通过对事件逻辑理论Lo ET公理系统以及引理进行扩展,提出一种改进的理论Lo ET-E并使用Lo ET-E对协议的安全属性进行验证,使事件逻辑理论适用于新兴协议。本文主要研究成果如下:1.规范事件逻辑理论中基本建模理论,包括事件序,事件类以及事件结构的相互关系,详细刻画挑战数及其基本性质,分析事件逻辑理论公理系统,完善七种基本动作类以及协议形式化定义。2.基于事件逻辑理论提出一种用于证明协议安全性质的改进理论Lo ET-E,扩展现有事件逻辑流关系公理中has的定义;扩展诚实公理,重新定义诚实主体可接收签名的来源,完善协议发生过程中可能发生的情况;引入概念Fresh以及两个衍生概念Gen和First Send,并根据这三个新概念提出了一系列重要规则。3.在Lo ET-E的基础上引入三个新的概念Safe,Safe Send和Safe Net,并根据这三个概念提出一系列公理规则和推论,构成可用于证明机密性的机密性证明系统,将Lo ET-E可证明安全属性扩展到机密性。4.使用Lo ET-E对基于PUF的双向认证协议的安全性进行分析,根据PUF安全性实现原理首次通过Lo ET-E抽象化PUF功能,使用基本序列定义协议双向认证过程并进行排序,对双向认证协议的安全属性进行刻画,最后使用Lo ET-E公理系统验证其强认证属性,得出基于PUF的双向认证协议在合理假设下是安全的,说明Lo ET-E可用于证明双向认证协议中不同性质主体间的认证性。