教学课程资源库 更多>>

关键词： 基站维护   基站检测系统   J2EE架构   结构化设计  

摘要： 中国移动和中国联通是我国移动通信领域的两大运营商，最近几年，它们的网络规模随着我国移动通信的不断发展已经临近饱和。简单的接入服务已不能满足广大用户的多样化需求。现今，移动运营商需要更高质量的网络服务和更多的网络种类。运营商已经变革了对网络管理的方案，更多的是重视了对网络性能指标的定量管理，而不再像以往那样只注重信号覆盖的定性要求。总体而言，我国的移动通信有了跨越式的发展，已经进入了网络管理与优化阶段，而不再停留于网络建设阶段。 这种情形下，各大运营商最为关注的头等问题必然是如何通过合理的配置网络资源从而提高网络的服务质量，只有这样才能提升这类企业的存活能力。而合理的配置网络资源也是网络维护的重要范畴，因此，研究网络维护有重要的现实意义。本文设计的基站维护检测系统基于J2EE框架，同时利用WEBGIS平台的应用理论，实现了基站维护过程业务模块的电子化操作。无论对于基站工作人员还是基站管理者、通信公司，基站维修检测系统都具有巨大的作用。对于工作人员来说，该系统实现了基站的设备与软件的联机，工作人员不必亲自去现场就可以知道基站设备是否正常工作，而且工作人员手工记录日志的麻烦也解决了，提高了工作人员的工作效率，减轻了工作量。而对于基站管理者更是最终的受益者，管理者只要轻松的登录软件就可以了解最近的基站工作情况，对基站的日常情况更是方便、快捷的提出意见。

关键词： 时序逻辑   断言图   形式化方法   模型检验  

摘要： 由于因特网和嵌入式系统在汽车、飞机以及其它安全系统的成功应用，未来将会更加依赖于计算机设备的功能。由于技术的快速发展，发展验证系统正确性的可靠方法变的越来越重要。目前用于复杂系统的有效方法包括仿真验证、测试验证和形式化验证。前两者验证花费的时间空间长、不易使用，并且无法做到对所有可能性输入和潜在的缺陷进行验证。形式化验证使用数学的方法证明给定的系统模型是否满足要求，从而做到了对用例的全覆盖。形式化验证又包括了形式化等价验证、推理验证和模型验证。模型验证是一种用于验证有限状态并发系统的技术，它对系统建模，并验证系统是否满足规格说明。时序逻辑如 CTL、LTL是目前常用的规格说明语言，基于 CTL、LTL的模型检验广泛应用于工业中。GSTE是一种高效的自动化模型检验算法，使用断言图作为规格说明语言。断言图较时序逻辑更易于使用，而 LTL与断言图在描述方面更为接近，因此，将 LTL转换成断言图有着实用的意义。　　本课题从形式化方法的基本概念出发，对时序逻辑和断言图进行了对比其优劣势，并对断言图进行了扩展，针对课题进一步的扩展，提出了扩展的验证算法，使得算法能够验证扩展之后的断言图并利用其性质验证了算法的正确性和完备性。　　本文首先介绍了形式化方法和模型检验的概念，给出了课题的研究意义，其次详细的介绍了广义符号轨迹赋值的验证过程，引入了其规格说明语言断言图，再次本文介绍了LTL、CTL及基于这些时序逻辑的模型检验算法，对比了CTL与LTL之间的区别和联系，然后对比了 GSTE和基于时序逻辑的模型验证算法，将时序逻辑转换成 Büchi自动机，并将 Büchi自动机转换成断言图，从而达到将时序逻辑转换成 Büchi自动机的形式，在这过程中说明了断言图的局限性。本文基于广义符号轨迹赋值的相关性质引入终端的概念，基于断言图定义了终端断言图，并将强满足算法进行扩展，提出终端可满足性算法，使得其能验证终端断言图，本文给出了终端可满足性的相关性质，并使用数学推理证明了终端可满足算法的正确性和完备性。在文章的最后，通过模型对性质进行验证满足性的过程说明了终端可满足算法的计算过程。

关键词： 民航空管系统   设备运行保障管理系统   UML建模   数据建模  

摘要： 近年,我国民航运输生产飞速发展。随着中国现代化进程的日益加快,我国民航空中交通管制(简称“空管”)行业步入了持续快速发展的黄金时期。通过我国民航事故统计可以看到,绝大多数安全事故都与交通管制直接或间接相关。作为民航的一个子系统,空管设备运行保障管理系统是有效维护空中交通安全和畅通的重要保障。目前,我国空管系统中设备运行保障管理系统的不健全问题日益凸显,成为制约我国民航业发展的瓶颈。 本文根据民航贵州空管分局各运行部门的实际情况,提出了跨地区、成系统的设备运行保障管理系统的建设方案与措施,以期能为贵阳民航空管系统的设备运行保障管理系统建设发展提供新的思路与参考。 论文首先介绍了民航贵州空管系统的设备运行保障管理系统的研究背景,对所需要解决的问题进行了概述,讨论了项目的研究意义与重要性,阐述了系统开发方法和相关技术；论文提出了系统的设计目标,对系统进行了详细的需求分析,包括业务需求、功能需求、数据需求和非功能需求,给出了系统的业务流程图、用例图和概念类图,进行了用例描述；在系统设计中,对系统进行了总体设计与模块设计,包括系统权限管理、部门岗位及人员管理、设备信息管理、值班管理、交接班管理、设备巡视／维护管理、系统查询、系统维护日志、用户界面等功能模块,给出了模块设计的功能结构图(包图)、类图、顺序图(协作图)和处理流程图,详细阐述了设计内容,进行了界面设计,并使用实体类图、E-R图和数据库表结构对数据库进行了详细设计；论文最后对研究的内容进行了总结,阐述了本人的主要工作,指出了论文存在的不足,并对进一步的工作进行了展望。

关键词： 无线电频率台站管理系统   分析   设计   uml建模   数据建模  

摘要： 随着无线电新技术、新业务的不断推出和应用,无线电技术已广泛而深入地进入到经济和社会生活的各个方面,在经济社会发展和国防建设中发挥着越来越重要的作用,而随之带来的是频谱资源日趋紧张,无线电干扰日益严重,电磁环境越来越差,为更为充分的使用无线电频谱,提高保山市无线电管理水平,建设一个功能齐全、性能稳定且适合保山市实际情况的无线电管理信息系统,是为保山市无线电的科学管理提供强有力的技术支持,也是促进社会经济发展的迫切要求。 本论文根据国家无线电管理办公室和云南省无线电管理部门对无线电管理系统的指导意见,借鉴相关领域的经验,从保山市无线电管理的工作情况和实际出发,对系统的业务范围、功能需求、体系结构等全面的分析和设计。论文首先介绍了保山市无线电频率台站信息管理系统的研究背景,和现存无线电管理中存在的问题,经过对国内外无线电管理的现状的分析,对系统开发的意义和重要性进行阐述。并概述了本系统开发中所用到的方法和相关技术,根据本文提出的设计目标采用业务流程图、用例图等对系统进行业务、功能、非功能等需求分析,并根据需求分析通过功能结构图(包图)、类图、顺序图和流程图详细阐述设计的内容,利用类图、E-R图和数据库表结构对数据库进行详细的设计,最后是对本次研究进行了总结,对此次开发中存在的不足之处做了说明,同时对无线电管理工作做了进一步展望。

关键词： 企业级应用   系统化复用   特征建模   模型驱动的开发   基于构件的开发  

摘要： 随着全球化竞争的加速,企业级应用作为当前信息技术应用的一个主战场,在软件规模的不断增长、交付周期的不断缩短的情况下对软件开发与交付带来了巨大挑战,如何基于可复用资产进行高效的开发成为当前企业级应用软件开发面临的关键问题。虽然四十多年的软件复用研究与实践在软件开发方法、过程与工具方面对提升软件生产水平有了质的飞跃,但由于软件本身的内在特质还未被人们充分了解,其典型表现就是“软件危机”一直存在。本文以企业级应用开发为研究对象,利用软件产品线开发的思想,将模型驱动的开发与基于构件的开发方法以集成化框架的方式融入企业级应用的复用开发过程,完成了如下实用且有新意的工作：(1)针对企业级Web应用开发(尤其是UI)工具支持不足、代码混乱、不易复用等问题,提出了基于架构模式的Web应用层次化模型及其描述语言,将企业级应用进行以架构模式为基础的模型化开发,从而a)易于结构分析与复用：b)易于工具支持的实现；c)有助于提升可读性。进一步的,从Web应用开发的实践出发,以UI建模为主导,通过构件化、面向对象的精化、参数化形成可复用领域模型制品,形成UI驱动的模型化复用开发方法,通过人工与自动化的UI建模相结合最大限度的发挥两者的优势,克服单纯的自动化建模对定制支持不足的问题,提升了开发效率。实践证明该方法可以显著的提升应用的开发效率。(2)针对Frame技术(XVCL)强调通过预处理器指令来标识程序中的共性模式和可变性,以消除冗余代码,但却导致frames构件边界不清、新需求的融入导致重构维护困难的问题,提出了一种Frame和逐步精化相结合的构件演化开发方法。其基本思想是将“特征”作为关注点分离需要考量的维度融入Frame构件的设计之中,使得frames融入了逐步精化的语义；进一步的,揭示了Frame与逐步精化深入融合的相关问题,为构建统一的以frames为基础、面向特征的软件开发方法奠定了基础。将Frame与逐步精化相结合,有助于精化中细粒度的可变性特征标识,提升frames设计中的关注点分离,促进基于Frame的软件开发。(3)针对特征模型在表达能力、可扩展性、模糊语义等方面的不足,提出了一种文本式特征建模语言—TEFL。TEFL具有严格的形式化语义,支持高级特征表达,提供了特征片段的模块化组织与复用,消除了既有语言表达法的不足。进一步的,以TEFL为基础,提出了基于特征的构件适配组装方法,实现了特征在代码层的映射,提供了对构件进行面向特征的适配与组装,使得特征模型不仅用于模型分析,还可以用于开发与代码生成,形成以构件技术为基础的软件产品线方法,有利于特征模型在工业界的导入。(4)针对企业级应用开发中模块化支持不足,既有应用难以形成基于业务粒度的构件的问题,提出基于OSGi的企业级应用构件化开发、运行、部署方法。该方法提供了用于实现企业级应用构件化的阶段性技术方案。开发期构件化借助Eclipse环境采用企业级应用特定的构件模型来进行开发,通过部署期架构转化实现构件化开发系统向传统Java EE系统的转换；运行期构件化采用了OSGi构件与传统JARs“混搭”的技术框架,其基本思想在于不同类加载器的融合,实现了业务构件的运行时动态化管理,简化了企业级应用向运行时构件化过渡的成本。

关键词： 半结构化   中医   电子护理文书   数据库系统   护理信息   电子病历   基本信息   患者   护理管理   病历模板   信息化系统   护士工作站   自动采集   准入控制   信息录入   系统模块   临床护理   就医过程   护理记录   控制包  

摘要： 护理电子病历是电子化的护理文书记录，是患者就医过程中所有护理信息的表述。我院历时2年将临床护士工作站、护理管理信息化系统逐步建立完善，特别是中医电子护理文书的实施使临床护理、护理管理更加高效、科学。护理电子病历是集成于CIS系统的护理信息系统模块，该系统包括自动采集患者基本信息（如患者姓名、性别、年龄、住院号等）、录入和存储护理信息、查看并打印护理记录等功能，主要采用全结构化和半结构化的信息录入模式。1电子护理文书设计
　　1.1电子护理文书的流程控制包括病历数据库系统和模板数据库系统。病历数据库系统是患者基本信息和护士的准入控制，模板数据库系统主要是电子病历模板的制作和维护。

关键词： 无线设备   管理组件   数据库系统   UML建模   ACE  

摘要： 从笔记本、上网本到手机、家庭高清播放器，日益丰富的网络应用让互联网与人们的联系越发紧密，而以无处不在、无时不在为标志的无线网络正逐步改变人们网络生活方式，提供无线服务的无线网络设备也必将走进千家万户，渗透到人们的日常生活中。高性能的无线设备管理软件也就应运而生。如何高效的管理无线设备，将是信息化建设不可或缺的议题。 Protocol Buffers作为数据存储和传输的载体，轻巧高效，信息容量大，易扩展，被该组件作为无线网络中所有可能的被管理对象的集合的数据存储结构。 目前比较优秀的的基础设施中间件， ACE （Adaptive CommunicationEnvironment）已经被广泛使用于网络软件开发；它提供了一系列面向对象的框架，实现了许多用于并发通信软件的核心模式，能极大的简化项目组织的复杂性，加快项目进程。因此作为此次开发的最好选择。 该组件是一款建立在iMC平台上的无线设备管理组件，以惠普无线业务驱动为中心，按照软件工程方法，对组件进行需求分析，并运用面向对象建模技术，逐步给出组件的用例图、时序图和逻辑视图，最后完成了业务分析和组件的总体设计。通过将系统分为设备基本信息读取模块、设备实时统计信息读取模块、设备配置管理模块、设备通信管理模块等四个主要模块进行了系统的详细设计，包括数据结构的设计、基于ACE框架的关键类的设计和数据库的设计。组件采用了高效的，自动化的结构化数据串行化机制protocol buffers的数据传输机制，同时应用了ACE框架中的反应器模式实现与设备间的异步通信，提高了组件的性能和可扩展性以及管理人员的工作效率。经过系统测试，读取、配置和监控无线设备等基本功能均已实现，该组件性能一般、易维护、可扩展，基本达到客户需求。

关键词： 公文流转   电子政务   UML建模   协同办公  

摘要： 公文流转系统是从促进信息产业发展的需要,整合政务信息资源的需求出发,重在提高政务效率,充分利用计算机和现代通讯手段,建立政府内部信息交流的快速通道,共享信息资源,强化部门业务管理,加强各业务部门之间的交流,实现政务信息的快速上传下达,促进协同办公,提高办公效率,为各级领导及业务人员提供辅助办公和决策服务。通过单位的内部网络,利用公文流转系统将传统的公文人工呈报方式改为网上传递,加强后勤部的管理职能,缩短公文流转时间,提高办公效率。在公文处理环节中,着重对单位公文的内部流转进行精心设计。系统采用固定节点、组合流程的设计思想,使得公文的流转不受固定流程的约束,以增强了系统的适用性与延续性。 本文以东莞交警支队办公室收发文业务为研究背景,对公文的发文和收文相关逻辑进行分析和研究,对应用系统进行了需求分析。围绕发文拟稿、审批、印发,收文登记、办理、审批等业务流程分析了系统的功能需求,通过应用统一建模语言(UML)进行建模分析,提取系统的用例和参与者,以用例图的形式展现系统组成和各部分的关系。在系统设计中,对系统的总体结构、各模块功能和数据库进行了设计,分别给出了系统总体结构图、各模块程序流程图和E-R图,并详细设计了各关系表。

关键词： 形式化方法   联锁   安全规范   安全苛求系统   事件B  

摘要： 铁路信号的根本功能是保障列车运行安全、提高运输效率,车站联锁系统是铁路信号的核心技术装备,它通过对信号机、道岔和进路的控制来指挥行车、防止列车冲突。随着计算机联锁系统的应用推广,联锁系统对软件的依赖性越来越强,如何提高联锁软件的质量、确保系统安全是近年来轨道交通领域研究的热点问题。联锁系统安全规范的严格描述与验证对保障软件开发质量具有重要意义。 本文从我国铁路信号联锁逻辑控制电路入手,深入分析提炼联锁系统的安全规范,利用形式化方法进行严格的描述与分析验证,具体工作如下： 1.查阅大量文献,论文首先对形式化方法在铁路领域的应用进行了深入的分析和综述,阐述了联锁系统开发过程存在的规范表达二义性和不精确问题； 2.结合形式化方法的发展趋势,研究了普适性形式化规格描述与验证方法,并对当前流行的方法进行了分类总结,深入探讨了Event-B方法。 3.深入研究了6502电气集中联锁逻辑控制电路,结合站场图,重点分析了信号开放控制、四线制道岔控制电路、进路建立和分段解锁等联锁关键环节,提炼出关键环节的联锁系统的安全规范。利用逻辑语义和一阶谓词逻辑对安全规范进行了形式化描述。 4.结合具体的站场实例,基于Event-B方法,利用Rodin平台,对信号开放、道岔控制、进路解锁等联锁系统关键安全规范进行了形式化模型描述和验证分析,给出了严格的分析结果。工作表明,铁路信号联锁系统是具有复杂时序逻辑的控制系统,Event-B方法适合于该类系统的描述与验证。通过形式化的联锁安全规范描述与验证,可以在系统开发的早期及时发现设计错误或漏洞,有助于提高计算机联锁系统的软件开发质量。本文的工作,为现阶段我国铁路信号安全关键软件的开发提供了借鉴。

关键词： 网络式软件   需求验证   形式化方法   RGPS  

摘要： 需求验证一直以来都是软件开发过程中非常重要的一个环节，软件需求的正确性直接影响着后期开发工作中人力、物力和资源的消耗。随着网络技术的发展，一种部署在网络环境中的复杂软件系统—网络式软件产生了，其拓扑结构和软件行为可以动态演化，因此，对传统的需求验证方法提出了新的要求。形式化方法通过对系统进行严格的语法和语义定义，使得分析和推理能够精确化、数学化，从而能够完备的证明系统是否正确实现了设计者的意图。 网络式软件需求模型的验证主要针对目标模型和过程模型，在973项目“需求模型验证与管理”（2007CB310803）的支持下，本文针对网络式软件需求模型目标层和过程层的特点，充分利用已有的形式化规约语言和分析方法对其进行形式化方法的研究。主要工作包括以下几个方面： 1.针对因网络式软件复杂性而带来的需求获取信息不协调性难以避免的特点，提出应用极大协调子集的思想进行不一致信息的处理；针对处理后的信息，在目标层模型思想的指导下，建立了一种新的描述需求目标性质和目标之间关系的GM模型，给出了GM模型正确性和完整性分析方法，以及相关验证算法，并设计了动态环境下目标模型演化的相关规则。该方法可以刻画目标层中所有目标之间的关系，包括低层目标之间的关系和高层目标之间的关系，并能融合用户需求之间的不一致信息，保留需求初期还未能确定的系统目标。 2.在深入研究Z语言和Petri网特点的基础上，扩展了集成Petri网和Z语言的PZN模型，并将它应用于网络式软件需求过程模型的建模分析，给出了PZN模型的活性、可达性和完整性具体分析方法，基于PZN模型对过程模型进行形式化建模和分析，利用PZN中所含的Petri网性质分析过程模型的活性和可达性，通过PZN中的Z框架描述分析过程模型的完整性，同时，给出了动态环境下，过程模型的增加、减少、模块划分等变化规则。 3.为了保证过程模型同已确认的需求目标及业务规则的一致性，在分析原子目标和原子过程的映射关系的基础上，分析了整个目标模型与过程模型间的相互关系，提出了目标层与过程层的一致性定义及其分析方法，以保证过程模型能够正确的实现用户需求目标，以及需求分析过程中目标与过程的统一。 本文在网络式软件需求验证的形式化方法上的研究成果，能有效的刻画用户需求的功能属性和非功能属性，有利于提高需求分析阶段的正确性和完整性，降低软件中因为用户需求的不正确而带来的错误以及资源的损失，提高软件开发的效率。同时，本文作者参与了所在团队网络式软件需求模型验证器的开发，实现了本文中的需求验证方法，并对项目实例进行验证，实例显示本文的方法具有很好的效果。