教学课程资源库 更多>>

关键词： 中山学院   学籍管理   信息系统   需求分析   UML建模  

摘要： 学籍管理是学校依据教育部学籍管理办法,结合学校自身办学特点,对学生在校期间学籍信息情况进行的管理和维护工作。高校学籍管理是教学管理实务中不可或缺的一部分,随着科学技术的发展,计算机辅助、数据库管理技术走进了大学教学管理,代替了传统的纯手工管理工作,大大减少了管理成本,提高了管理效率。 论文介绍了目前高校学籍管理系统的研究背景和应用现状,通过调研和分析完全学分制改革背景下高校学籍管理的基本要求,提出了基于完全学分制,中山学院学籍管理问题解决方案。 论文采用UML建模的方式,以面向对象的方法,对系统维护、学籍管理和查询打印三个功能模块,从业务分析、功能分析和数据分析三个方面对完全学分制下中山学院学籍管理系统的系统功能进行了全面描述。在业务分析中,论文对当前学籍管理存在的问题、学院组织机构进行了详细说明,对原有业务流程进行了分析,并给出了改造后的业务流程；在功能分析中,论文通过用例分析和用例描述,明确了系统的功能,并给出了系统的总体功能包图和子功能包图；在数据分析中,论文对系统各功能的所需要处理的数据进行了分析,给出了实体类关系图,建立了数据库表结构；论文最后对所做的研究与分析工作进行了总结,并对进一步的工作进行了展望。

关键词： 泉州经贸学院   学生日常管理   信息系统   需求分析   UML建模  

摘要： 论文首先介绍了科学技术发展与高校学生工作难度增加的研究背景与意义；对泉州经贸学院学生日常管理信息系统要解决的问题进行了概述,讨论了通过系统应用,提高学院师生管理工作的效率与项目的研究意义与重要性；接着通过软件工程可行性分析,对学生管理系统的实际需求分析存在业务流程,并对其重新改选业务流程；在系统的功能性与非功能性、数据库等,论文通过对用例分析与用例描述,详细说明系统的总体功能包图和子功能包图,包括学生基本信息、宿舍管理、荣誉管理、违处管理、毕业管理、系统管理、助学管理等子包图；在数据分析过程中,论文对信息系统功能需要的数据进行数据分析,结合学院学生日常管理信息系统,给出了实体类关系图,对数据库结构进行了系统设计。论文最后对研究的课题总结,阐述了本人的主要工作,指出了论文系统安全性、电子签章等方面存在的不足与今后展望。

关键词： 实时时序逻辑   TMSVL   形式化方法   模型检测   CTCS-3  

摘要： CTCS-3(China Train Control System level 3)级列车控制运行系统是保障我国铁路时速300～350 km客运专线高速列车安全、可靠、高效运行的核心技术之一。然而,对于列车控制运行系统这种实时安全关键系统,仅仅依靠经验和自然语言来制定和描述系统的需求规范会难以避免的存在某些缺陷和不安全因素,并且系统的测试若都以现场跑车为主,也会消耗大量的时间和精力。因此,需要一种技术来验证这种实时系统的特性,从而提高系统的正确性或完善系统的功能。基于严格数学定义的形式化方法,由于其能够简洁、准确的描述系统的规格,并验证系统的特性,因此能够作为系统建模和验证的重要理论方法。而时序逻辑作为一种形式化方法,近些年来已经被广泛的运用于实时系统的建模和验证中。实时建模、仿真及验证语言(Timed Modeling Simulation and Verification Language,TMSVL)是一种基于实时投影时序逻辑(Timed Projection Temporal Logic,TPTL)的实时时序逻辑程序设计语言,它主要用于对实时系统规范的建模、仿真和验证。本文以TMSVL语言作为实时建模、仿真和验证的形式化语言,以我国CTCS-3级列控系统作为建模和验证的对象,提出了一种基于TMSVL语言的CTCS-3级列控系统运营场景形式化建模与验证的方法。文章首先介绍了TPTL和TMSVL的语法和语义,以及其执行平台TMSV(Timed Modeling Simulation and Verification platform,TMSV),然后简单介绍了CTCS-3级列控系统的结构,并以CTCS-3级列控系统的规范文档作为建模的基础,针对CTCS-3系统规范中的一些核心的运营场景,使用TMSVL语言进行建模,使用实时命题投影时序逻辑(Timed Propositional Projection Temporal Logic,TPPTL)语句描述实时性质和安全性质,最终在其建模和验证环境TMSV平台中完成了CTCS-3级列控系统的建模、仿真和验证。

关键词： 混成系统   形式化方法   混成自动机   接口自动机   Z语言   互模拟   模型检测   精化检测  

摘要： 混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,针对混成系统的形式化建模与验证是确保其正确性和可靠性的重要途径。混成系统不仅含有复杂的动态行为、时间限制,还包括与外部环境的通信等特征,针对混成系统的形式化规范技术必须能够描述所有这些方面,但是单一的规范技术很难适合这样的应用场景。在具体分析和验证混成系统时,由于混成系统状态空间是无限的,关于混成系统的诸多研究问题(可达性问题、模型检测等)都是不可判定的。本文主要包括如下四个方面的研究工作。(1)本文基于描述系统行为各个方面这一想法,首先组合了三种已经被广泛研究的规范技术:接口自动机、多速率混成自动机和Z语言,称为多速率混成ZIA规范,该规范不仅可以描述多速率混成系统软件组件接口性质、混成时序性质,还具有很强的描述数据性质的能力。(2)本文给出了连续时间ZIA规范上的互模拟关系定义,不仅考虑行为间的互模拟关系,还考虑了数据间的互模拟关系;然后,基于有限论域CT-ZIA规范,给出了其上的互模拟检测算法,并对算法正确性进行了说明。(3)本文提出了针对多速率混成ZIA规范(MZIA)的带数据约束时序逻辑,考虑到实际应用中对混成系统中连续变量的测量存在误差,该逻辑可以刻画MZIA规范“近似满足”满足某个给定的系统性质;接下来,提出了针对多速率混成系统的一种近似模型检测算法,用来判定一个MZIA规范描述的系统是否近似满足某个带数据约束的时序逻辑公式描述的性质;最后,通过对锅炉系统的例子详细展示了MZIA规范的建模过程以及其上的近似模型检测步骤,说明了本文方法是可行和有效的。(4)本文给出了多速率混成ZIA规范上的精化关系的定义,这种精化关系不仅考虑了动作行为的“交替模拟”,还包含了数据间的精化关系;然后,提出了针对有限论域MZIA规范的精化检测算法,该算法可以自动验证系统的规范到实现的正确性;最后,基于锅炉系统实例展示了精化检测的具体过程。

关键词： 人口管理   申报   UML建模   信息系统  

摘要： 深圳是典型的移民城市,人口结构中非户籍人口比重远远大于户籍人口,非户籍人口管理一直是深圳公安机关的人口管理工作面临的重大课题。过去曾经实行暂住证制度,现在实行居住证制度,但在非户籍人口管理上归根到底是要靠居住登记来实现。过去,深圳市非户籍人口的居住登记工作,由“出租屋和流动人口综合管理所”逐门逐户上门开展。目前深圳市正在进行有关非户籍人口在深圳经济特区居住的有关立法研究,准备在深圳实施非户籍人口居住信息的申报制度,由住房提供者履行申报义务。基于上述情况,本人在学习软件工程课程的基础上,分析和设计网上非户籍人口居住信息申报系统。 本文就非户籍人口居住信息申报系统研究的选题背景做了介绍,提出了居住申报工作在信息系统方面所面临的问题,指出了软件的设计方向；然后,本文从业务、功能、数据等几个方面出发进行了充分的需求分析,运用UML活动图对业务需求进行了描述,运用UML用例图对功能需求进行了分析,运用概念类图对数据需求进行了说明；在系统分析的基础上,本文给出了软件的总体结构设计和网上申报、搬离注销、核实管理、抽查管理等各个功能模块的设计以及数据库设计,通过UML包图、类图、顺序图、处理流程图、实体类图、实体类关系图和数据库表结构等方法对设计进行了具体描述；最后本文对研究工作做了简要的总结和展望。

关键词： 浅议   结构化设计   道路桥梁设计   应用  

摘要： 随着我国经济的飞速发展，交通运输业也获得巨大的发展与进步，道路和桥梁的建设就显得尤为重要，而结构化设计对道路桥梁来说至关重要，结构化设计不仅要考虑道路桥梁建设所在地点的交通运输情况，还要考虑其实用性，因此，本文就道路桥梁结构化设计的重要价值、结构化设计的不同计算模型、结构化设计方法在道路桥梁设计中应有的重要性研究及应用原则及道路桥梁结构化设计应该坚持的原则进行分析。

关键词： 图书馆   开放式借阅管理   信息系统   需求分析   UML建模  

摘要： 高校图书馆是校园信息的传播中心和集散地,伴随着高校的扩招,图书馆的藏书量迅猛增加,馆舍面积不断扩充,借阅管理中产生的信息量日益庞大。而高校图书馆当前正在使用的一些借阅系统的部分业务子模块还没有应用到或者说还不够完善,从而,使图书馆管理信息系统的强大功能没有能够完全的发挥出来,将原有系统进行再造,对进一步方便教师和学生以及提高图书馆工作效率都具有重要意义。 本文结合工作实际,使用软件工程面向对象的研究方法对云南大学图书馆开放式借阅管理系统进行了详尽的研究与分析。文章的开头介绍了该系统的研究背景、项目意义和现阶段的研究与应用现状,确定本论文研究的主要内容和工作；首先,本文从原有系统的组织机构、业务描述、业务问题和业务流程几方面进行了详细的业务分析,画出了重组后的业务流程图；其次,对该系统进行功能分析,通过用例分析与用例描述,确定系统功能,画出系统总体功能包图与子功能包图,包括：图书借阅管理、图书归还管理、书证管理、图书信息管理、远程应用管理和系统管理6个功能模块。再次,对系统进行数据分析,详细分析系统各功能需要处理的数据,画出实体类关系图,建立数据库表结构；最后,总结本次的研究与分析工作,并对将来的工作进行展望。 该系统的再造改变了原有工作中,图书馆馆员花费更多时间和精力来工作和服务的模式,使图书馆借阅管理更加规范,远程应用模块的再造,彻底打破了时间与空间的限制,体现了时空开放观,使读者使用图书馆更加方便、快捷,对云南大学图书馆当前的图书借阅工作起到了有效的补充和支持作用。

关键词： 体系结构   层次聚类   共性挖掘   频繁子图  

摘要： 近些年来体系结构的设计发生了许多变化，从原来的单核到现在的多核以及集群的设计，这种变化的一个重要目标就是满足应用的计算需求。然而应用的多样性以及差异性使得这种“one fits all”的体系结构设计哲学变得不可能，同时一些新兴应用环境（嵌入式领域以及移动智能设备，如手机，数码相机）的出现也给传统体系结构的设计带来非常大得挑战，传统体系结构在适用于这些应用背景时所面临的一个非常难解决的问题就是无法满足它们在性能，功耗以及成本上的严苛要求。为了满足应用在性能以及功耗方面的需求，我们必须要针对每一个应用程序进行专门的分析，挖掘他们的内在特征和算法本质，进而根据这些特点设计专门的体系结构，于是领域专用的体系结构设计便在这种大环境下应用而生。这种专用结构所带来的性能提升以及功耗降低主要得益于它里面针对特殊计算流程所定制的硬件功能模块。然而在领域专用的结构设计里面一个关键而困难的问题便是如何自动化的实现专用体系结构的设计，并获得有效性以及灵活性的平衡，概括起来有以下两个问题需要回答:　　1.给定来自于一个领域或者多个领域当中的一组程序，我们需要设计多少种定制体系结构才能满足应用的加速要求　　2.对于每一个结构类别，它最关键的计算结构是怎样的，什么样的算法模式才应该定制为硬件加速单元　　在本论文当中我们针对多个程序组成的集合按专用加速体系结构适应性分类和共性可加速操作的生成问题，提出一种全自动化的解决方案。该方法注意到了领域应用之间存在的相似性，使用频繁子图挖掘的方法来识别多个应用之间的公共计算操作，并将这些公共计算结构定制为扩展的指令。这种共性挖掘能够充分揭示领域应用之间的核心操作结构和关键计算模式。本论文方法的技术优势在于:　　整个流程通过频繁子图挖掘的机制实现了完全的自动化，不需要任何的人工参与。本发明可在使用者对于目标应用程序集完全不了解的情况下挖掘关键结构;本论文充分利用了领域当中各个应用之间的相似性来挖掘多个应用之间频繁出现的主流计算结构，这也就保证解决了方法的可重用性以及灵活性;本技术能够将来自不同领域背景的应用程序分类到少数几个高内聚性的分组当中，从而约减了硬件加速电路设计的复杂度。　　本论文的主要创新点在于:　　基于算法内在相似度的程序分析流程　　对输入的一组源程序程序进行自动化的分析，不需要任何的人工参与以及指导，最终生成高内聚性的分组，以及每一个分组关键的计算结构和算法模式。　　算法内在相似度的度量指标　　能够将算法相似性这种抽象的东西建模，具体化为公共子图的集合，同时提供了一种量化的手段来衡量应用相似性的程度，领域相似性的程序以及领域当中应用相似性的波动情况等，为后面基于算法内在相似性（公共计算结构）的聚类提供数学基础。　　基于频繁子图的共性操作提取算法　　实现了数据流图中的频繁子图挖掘，从而提取多个应用程序当中的公共操作和相同的计算结构。　　针对领域专用加速的程序聚类算法　　针对领域专用的加速器设计，将来自同一领域或者不同领域的多个应用根据算法相似性进行分类，并提供每一类当中的关键计算结构和特点，从而约减设计空间，为设计者提供直接的指导和建议。

关键词： 高校奖助学金管理   面向对象设计   UML建模  

摘要： 随着高校信息化建设的不断深入,高校奖学金、助学金管理信息化建设已经成为完善、规范高校奖助学金管理的重要举措。本文结合云南交通职业技术学院奖学金、助学金管理现状,深入分析了当前高校奖学金、助学金管理面临的问题和信息化需求,并运用软件工程面向对象设计方法,在用例分析基础上,详细设计了学生信息管理、奖助学金项目管理、奖助学金申请管理、奖助学金审批管理、学生诚信管理、奖助学金发放管理以及财务统计的功能,同时对系统中每一个功能模块的操作流程进行了描述。通过本文的研究,利用信息化管理方式对高校奖学金、助学金管理流程进行了重新设计。从而进一步规范了高校奖助学金评审过程,切实加强了高校奖学金、助学金管理的质量和水平。

关键词： Energy efficiency  

摘要： Energy saving is a crucial concern in embedded real time systems. Many RT-DVS algorithms have been proposed to save energy while preserving deadline guarantees. This paper presents a novel approach to evaluate RT-DVS algorithms using statistical model checking. A scalable framework is proposed for RT-DVS algorithms evaluation, in which the relevant components are modeled as stochastic timed automata, and the evaluation metrics including utilization bound, energy efficiency, battery awareness, and temperature awareness are expressed as statistical queries. Evaluation of these metrics is performed by verifying the corresponding queries using UPPAAL-SMC and analyzing the statistical information provided by the tool. We demonstrate the applicability of our framework via a case study of five classical RT-DVS algorithms.