教学课程资源库 更多>>

关键词： PLM   项目管理系统   生命周期管理   Spring MVC框架   UML建模  

摘要： 随着经济全球化的发展,我国作为世界制造的中心,制造业企业面临这日益激烈的市场竞争。通过信息化手段来提升核心竞争力,研发出更新更好的产品,能够缩短开发周期,有效地增加收入和降低成本。目前MW公司研发项目管理面临这产品种类多、研发管理体系复杂、技术转化成产品周期长、研发人员众多等局面,传统的粗放式研发管理模式已经不能满足研发管理工作的需要,而且会存在各种风险。为了提高研发项目管理效率,促进产品设计到制造全过程的有效监管,因此本课题研究的PLM项目管理系统的构建具有十分重要的意义。本学位论文首先分析了PLM项目管理系统建设的主要背景,指出了系统建设具有非常重要的应用价值,阐述了课题的研究现状,对论文组织结构进行概述。然后对系统开发使用的Spring mvc、Hibernate、Hibernate、***、UML建模等技术,介绍了技术特点与工作原理。然后采用功能用例图描述了系统重要的业务功能,分析了系统核心业务流程,并指出了系统非功能性需求。本论文指出了系统设计思路,整体设计了总体架构、技术架构等架构,指出了PLM项目管理系统应用层次和关键技术,然后设计了系统功能结构和网络部署情况,明确了系统功能构成和硬件构成,并从E-R概念模型和数据库表结构物理模型两个方面进行了数据库设计。本论文重点阐述了详细设计和实现了系统登录、项目信息管理、项目计划管理、任务管理、项目成员管理、项目文档管理、产品结构管理、项目动态管理等功能模块。最后,介绍了系统的数据完整性、功能、性能等方面的测试过程,确认系统可以发布上线。本论文的研究给MW公司产品研发项目实施和管理提供良好的信息平台,有效缩短了项目实施周期,降低了产品研发项目成本,实现了产品研发项目过程可视化管理,实现了研发项目流程、数据、系统的统一,确保项目按照标准化、流程化方向实施,实现精益化管理,从而提高MW公司产品的市场竞争力,提高企业的经济效益。

关键词： 设计模式   模式组合   操作优化   形式化方法   等式推理  

摘要： 设计模式是软件设计经验的总结,恰当使用设计模式可以有效提高软件系统的可复用性,提高软件维护效率。在实际应用中,由于软件需求的复杂性,设计人员很少使用单一的设计模式,而是根据具体的应用场景和以往的设计经验,将多个设计模式组合使用。但是在这种缺少理论支撑和严密推导的情况下,模式组合结果的有效性无法得到保证,可能会对软件产品的质量造成不良影响。因此使用形式化方法准确地表示模式组合并判断这种组合方式是否有效显得至关重要。通过对比现有的模式组合形式化方法,发现操作符方法能够有效地展示模式组合后的结果,但是该方法仍然具有缺点:限制操作符与展平、提升操作符存在语义重叠。针对上述操作符方法中存在的问题,本文的工作具体如下:(1)结合模式的抽象逻辑规范与Z语言对操作符方法进行优化,在现有的操作符基础上提出了新的限制、叠加、扩展和泛化操作符。(2)探讨了优化后的操作符满足的代数法则,并采用代数推理验证了优化后的限制、叠加、扩展和泛化操作符可以有效的替代先前的限制、叠加、展平、泛化、扩展和升降操作符。通过减少操作符的数量,降低了多模式之间的语义重叠关系。(3)对优化后的操作符进行保存属性分析,总结出了判断模式组合是否具有有效性的方法。通过面向模式的实际案例验证了该方法的正确性,同时对比说明了本文优化后的操作符方法在去除操作符重叠方面要优于前人提出的方法。

关键词： 内控信息化技术   研究方法   形式化的具体方法  

摘要： 伴随着现在经济发展得越来越快,一些企业内部开始实施信息技术手段来进行内控管理,其中包括制定一些规范制定和企业流程具体的措施方案,以此来完成我们将信息化系统提高到企业内部需求的信息化管理平台的高度。早在二零零二年以后开始,美国自从颁布了萨班斯法案以后,各个国家开始对内部控制的认识达到了一个非常高的高度,与此同时我们国家在二零一零年开始,先后颁布了相关类型的文件,以此标志着在我国企业内部信息化体系正式完成。由于我们掌握度理论多于实践,这其中很多的地方还存在着一定的问题需要我们解决。

关键词： 逻辑运算   逻辑函数   表示方法   问题牵引教学法   课堂教学设计  

摘要： 该文结合问题牵引教学法和实验教学法学习三种基本的逻辑运算,同或、异或逻辑及逻辑函数的表示方法。逻辑运算是本次课的重点内容,以EWB仿真和实际案例突出本节课的重点;逻辑函数及其表示方法是本节课的难点,以同或、异或逻辑为依托讲授逻辑函数的表示方法,帮助学员攻克难点。实践证明本文提供的课堂教学设计有助于学员对教学内容的掌握,且有利于提高学员自主学习及分析解决问题的能力。

关键词： 形式化方法   自然计算   膜计算   软件产品线   软件演化  

摘要： 自然计算是模拟自然界的结构、功能或者层次关系等的一系列计算模型与算法。按照计算模型的启发源分类,自然计算可以分为物理层次、生命层次和文化层次的计算模型。计算机领域中常见的遗传算法、蚁群算法、神经网络等都属于生命层次的自然计算。膜计算作为一个近些年发展迅猛的自然计算分支,在理论和应用上均有很好的发展。本文基于膜计算相关理论,提出了两种新的膜计算变体并对这两种变体的应用进行了研究。服务组合中的孤岛问题需要实现孤岛与系统的通信,即系统与外界环境的交流。而软件产品线的演化问题需要实现在已有的系统中添加新的变化机制这个过程。已有的膜计算模型无法解决这两类问题。因此,本文在已有的膜计算理论研究的基础上,通过对膜计算中主要研究对象进行扩展,提出了适用于解决服务组合中孤岛问题的通道膜演算以及适用于对软件产品线演化问题建模的通信膜演算。本文的主要研究贡献总结如下:(1)已有的膜计算模型规定,对象和膜必须在同一表层膜内才能发生转移。这种定义意味着已有的膜计算模型无法描述两种不同环境之间的通信。因此,本文提出了一种新的计算方法——通道膜演算。这种方法对膜演算的反应规则进行了扩展,定义了对象和膜可以通过通道和膜进行通信的信息传递方式。在定义中,通道的建立并不局限于同一个表层膜,因此不同的表层膜可以通过通道进行信息(对象和膜)的传递。这种演算方法适合对孤岛问题进行建模。(2)已有的膜计算模型规定,对象和膜必须按照反应规则定义的方式发生变化。这种定义方式意味着这些方法的反应规则无法动态变化,因此不善于对变化方式不固定的系统进行建模。本文提出了一种新的膜计算变体——通信膜演算。通信膜演算在原有的膜计算模型定义的基础上增加了规则的传递、复制和删除的计算模式,使得反应规则也具有了动态变化的能力。因此通信膜演算比已有的膜计算模型具有更多的通信机制与变化机制。通信膜演算适用于对系统演化过程进行建模,如软件产品线的演化。(3)将本文提出的通信膜演算和通道膜演算与相关的膜计算模型进行了对比。利用后继状态和到达路径等概念,从静态结构描述能力和动态演化能力两个方面对几种计算模型进行了详细比较,对比结果表明:通道膜演算适用于对静态结构进行描述,通信膜演算适用于动态演化问题建模。(4)传统的软件产品线特征模型的构建大多依赖领域专家的分析,每当软件产品线发生演化时,领域专家都需要对特征模型进行重构。这个重构过程完全依赖领域专家对软件产品线和演化需求的理解,不能保证特征模型演化的正确性。因此,本文提出了一种基于演化需求的软件产品线特征模型自动生成方法,利用通信膜演算来描述特征模型的结构和演化过程。该方法利用通信膜演算抽象表示特征模型和演化需求,进而使得特征模型可以根据演化需求自动变化,得到演化后的特征模型。本文提出的方法可以自动确定软件产品线特征模型的演化范围,自动改变特征模型;可以减少特征模型演化过程中的领域专家的工作量,同时避免人为修正特征模型时产生的错误。

关键词： software inspection   SOLIMVA 3.0   formal methods   object-oriented reading techniques   quasi-experiment  

摘要： In this paper, we present a rigorous comparison of two inspection techniques: our formal method-based approach, SOLIMVA 3.0, with a set of Object-Oriented Reading Techniques (OORTs). We evaluated efficiency (required time to analyse a scenario) and effectiveness (ability to find defects within UML diagrams). Results show that the classical OORT methodology is more efficient than SOLIMVA. However, we found a strong positive correlation between the required time by using OORT and SOLIMVA. For effectiveness, in general, both methodologies presented the same performance. However, SOLIMVA detected more inconsistency (incorrectness and extra information), ambiguity, and partial incompleteness defects while OORT identified more total incompleteness. Our overall conclusion is that a classical reading methodology (OORT) and a formal-based one (SOLIMVA) can be adopted in a complementary way within a software inspection process. While OORT is less costly to apply, SOLIMVA can be used to address some specific types of defects.

关键词： 模型学习   形式化方法   时间自动机   寄存器自动机  

摘要： 形式化方法在模型为导向的软件工程中起到非常重要的作用,其中模型检验已经成为软件验证和纠错的一种重要方法,而模型学习是对于模型检验的一种有效补充技术。本文将对模型学习的概念和研究意义进行介绍,汇总了几种常见的对于寄存器自动机和时间自动机的模型学习的方法,并提出了一种对于时间自动机进行学习模仿的算法思想,最后对于模型学习的主要研究方向进行了阐述。

关键词： 车辆追踪系统   Spring boot   HBase   UML建模  

摘要： 在云计算、大数据等互联网科技高速发展的时代,计算机技术在各个领域中的应用越来越广泛,公安机关改变其传统工作模式以及业务流程已迫在眉睫。基于卡口数据的车辆追踪系统(下文简称车踪系统)作为公安厅信息化建设的重要组成部分,通过挖掘海量的卡口过车数据,为警务人员提供多种追踪车辆的功能,使警务人员追踪车辆更便捷高效,所以建设一个稳定安全的车踪系统尤为重要。论文选题来源于“炬云警务大数据”项目。本文通过采集某市各个卡口高清摄像头识别出的过车信息,对过车信息进行分布式存储,并充分挖掘卡口摄像头拍摄到的海量过车图片中包含的信息,针对警务人员遇到的实际场景,总结出近三十个简约高效的实战功能,使侦防工作模块化、桌面化,带动警务模式的转变。本文内容组织情况如下所示:(1)系统所需相关技术的概述。主要包括对Spring boot这一简化web项目开发流程框架的介绍以及对HBase、MySQL这两种本文使用的数据库进行介绍。(2)需求分析。通过调研公安厅警务人员对于建设车踪系统总体要求以及卡口过车数据内容,了解了车踪系统的需求背景以及目前卡口数据的存储方式,从而确定了本文系统的业务需求,通过UML建模的方式,使用数据流图、用例图、ER图的方式具体呈现。(3)设计车辆追踪系统的网络架构及逻辑架构。系统使用Spring boot技术,采用B/S架构,数据库使用MySQL和HBase两种数据来进行建设,将系统分为前端表现层、业务逻辑层以及数据持久层三层进行开发,保证了本文车踪系统的稳定、安全以及高性能。同时,将已确定好的系统功能模块化,并对各个模块分别进行详细设计,为保证车辆追踪系统的安全性,将系统统一部署在公安厅视频专网这一内网上。(4)设计车辆追踪系统中具体数据存储方案。首先,分别识别出在MySQL和HBase数据库中存储数据的实体,然后确定每种数据库中实体之间的关系,并给出实体关联关系ER图。在HBase数据库中,将车辆过车数据以不同的行键冗余存储,以提高不同检索条件的检索性能。在MySQL数据中,对表进行设计,将表结构进行说明。(5)依据设计好的方案对系统进行编码实现。依据每个模块识别出的类进行了模块类图绘制,并选取了每个模块中核心的功能点通过绘制序列图的方式进行详细说明。对实现好的车辆追踪系统进行充分的测试。通过对车辆追踪系统进行功能性测试和非功能性测试,保证系统可以完成需求分析阶段整理出的二十七项功能性需求以及并发量响应速度等非功能性需求,满足用户需求。

关键词： Conceptual model   database design   student design skills   UML notations   relational data model  

摘要： Background: Conceptual models are an essential phase in software design, but they can create confusion and reduced performance for students in Database Design courses. Objective: A novel Relational Data Model Validation Tool (MVTool) was developed and tested to determine (1) if students who use MVTool perform better than those who do not, and (2) if design skills improve after using MVTool. Method: After a pre-test of database design skills, 68 students were divided into matched-pair control and experimental groups. All completed a database design task, with the experimental group having access to MVTool and the control group having no access to the tool. Findings: Notable improvements in specific design skills could be consistently detected in students after the introduction of the tool. Implications: Validation tools such as MVTool may help students to understand modeling languages and conventions used in database design, thereby improving their skill development and course outcomes.

关键词： 形式化方法   定理证明   Coq   记录类型   矩阵理论   飞行控制系统  

摘要： 矩阵在理论数学、工程数学以及计算机科学中都有着广泛的应用。例如飞行控制系统的设计中,矩阵被用于飞行器受力状况的描述,运动学方程的推导,以及飞行控制算法的设计。因此,矩阵算法和矩阵数学推导的正确性对这类安全关键系统的可靠性有着极大的影响。形式化方法是保障计算机系统安全可靠的一种重要方法,其中定理证明技术可用于数学公式和计算机算法的验证,是最严格、最强力的验证手段。Coq就是这样一个交互式的高阶定理证明器,它基于归纳构造演算的基本理论,具有很强的表达能力,支持丰富的逻辑系统。Coq可用于表达规范说明,构造满足规范说明的程序模型,以及对可信性要求很高的程序进行形式化验证。虽然Coq中有着丰富的定理库,但是,现有的矩阵形式化方面的几种方案却不尽人意,基于List的方案表达能力受限,基于依赖类型List的方案复杂难验证,基于函数的方案只是验证了矩阵理论,不能构造出具有具体数据的矩阵,也不能用于实际矩阵的推导验证,并且不利于从描述中提取可执行程序。本文提出了一种基于Record类型的矩阵形式化方法,它具有描述上的简明性、证明上的简单性、使用上的简便性以及程序抽取的可行性等诸方面的综合性优势。本文主要研究成果如下:首先,提出基于Record的多态类型矩阵实现方案。该方法用记录的一个List类型的域来保存矩阵数据,用类型为Prop的域来保存一个关于矩阵大小的证明。这一矩阵定义方式,既能够保证矩阵具有指定的大小,又能够利用List类型实现简单的特性。在矩阵运算函数的设计和矩阵性质证明的复杂度上都比Coq中其它矩阵验证相关工作所采用的方法更简单。其次,研究了基于函子的独立于元素类型、具有通用性的向量和矩阵的形式化方法。函子是一种参数化模块,它可以看作是从模块到模块的函数。函子的输入参数的类型被称为签名,它描述了元素模块中的数据类型、在这种类型上的运算和这些运算所需要满足的性质。基于函子的矩阵能够利用输入元素的性质来证明矩阵的性质。常规的矩阵形式化方法需要对不同类型的矩阵分别进行形式化,借助函子,可以对各类矩阵进行统一定义,并对部分矩阵性质进行统一的形式化验证。接着,在函子向量和矩阵的基础上完成了实数矩阵、复数矩阵的形式化。同时实现了函数域的形式化,并在Coquelicot库一元函数定积分的基础上实现了二元、三元函数定积分的形式化。最后在前面工作的基础上进行了函数矩阵以及函数矩阵微积分的形式化描述和部分性质的验证。最后,我们通过飞行控制系统中坐标转换矩阵和运动学方程组的验证,来展示这个矩阵库的使用。可以看出,基于Record类型的矩阵使用简单,能够满足基础矩阵运算验证的需求。