教学课程资源库 更多>>

关键词： 形式化方法   CBTC   轨旁系统   Event-B   SCADE   建模与验证   精化   切片准则   Rodin平台  

摘要： 基于无线通信的列车自动控制系统(Communication based train control, CBTC)是新一代轨道信号系统。CBTC发车间隔短、轨道负荷大、运行平稳,大幅提高了城市公共交通的运载能力。为了应对日益严峻的城市交通问题,中国正加紧建设CBTC轨道信号系统。其中,轨旁系统是CBTC系统中安全需求最高的子系统之一。在实际情况中,一旦轨旁系统出现问题,会导致列车脱轨、碰撞等极为恶劣的后果。因此,在轨旁系统的开发过程中,保障系统安全性是极为重要的一环。然而,由于轨旁系统中的物理环境和系统行为比起传统轨道系统更为复杂,在验证系统安全的过程中极易产生状态爆炸问题。这使得轨旁系统的建模与验证工作困难重重。传统的开发方法没有引入降低模型复杂度的方法,显然不能满足大型系统的建模与验证需求。因此,在对轨旁系统进行建模与验证研究之前,我们必须考虑：如何降低模型的复杂度；如何对模型中的状态迁移进行划分；如何对系统的状态空间进行约减等一系列问题。同时,我们必须保证划分、约减后的模型与原模型之间的一致性。除此之外,我们必须定义并证明模型划分方法中的一些定理,使得划分后的模型能够在形式化方法的演绎系统中进行推理证明。在轨道信号系统建模领域中,Event-B方法和安全关键软件开发环境(Safety critical application development environment, SCADE)是主流的形式化方法,具有广阔的工业应用前景。由于大型系统中往往涵盖着复杂的状态迁移,所以对大型系统建模不能够一蹴而就。基于Event-B方法,我们能够在系统级直观地描述一个大型系统的所有行为,并且保证这些行为满足安全需求。通过Event-B方法的精化方法(refinement)我们能够逐步地引入系统的状态变量并强化模型中的事件约束,使模型逐步逼近实际的系统行为。同时,通过Event-B证明义务我们能够保证在不同精化层下,模型之间的状态变量保持一致。在安全关键软件的软件级开发过程中,基于SCADE方法,我们可以实现从模型设计、仿真、证明到自动代码生成的完整软件开发生命周期。基于该方法开发的软件具有较高的系统安全性,同时具备较好的可维护性。本文在Event-B精化方法的基础上,提出了模型的划分精化范式。该方法能够有效地降低模型的复杂度,使得状态空间约减后的模型能够被自动证明。首先,我们提出该方法的语法定义,图形描述以及推理演算规则。然后,对划分精化的证明义务进行了推理和证明,从而保证数学模型在约减前后状态的一致性。基于该范式,我们还提出了对大型系统的精化、划分、分解的迭代开发范型。为了实现该开发范型的自动化迭代,我们基于Event-B的建模平台Rodin开发了模型划分精化的插件。基于SCADE方法,我们提出了SCADE模型的切片准则,从而分割模型的状态变量空间。首先,我们给出切片准则的LUSTRE语法定义、基于时钟的数据流(data flow)的表达式以及相应的数学方程。通过对模型的状态空间进行切分,我们能够有效地解决SCADE模型在安全性质验证过程中的空间爆炸问题。最后,我们提出了基于CBTC的轨旁系统的形式化建模精化与验证方法。通过划分精化范式及插件实现,我们能够将轨旁系统的Event-B模型分解为低耦合的子模型,并在Rodin平台中完成轨旁系统安全性质的证明。在轨旁系统的软件开发过程中,我们基于SCAD E方法实现了模型驱动开发。通过SCADE运算符,我们形式化地描述了轨旁系统的物理环境和移动授权运算模块中的主要行为。为了防止状态空间爆炸问题,我们应用本文提出的切片准则对模型中的状态空间进行分解。最后,在Design Verifier工具中我们证明了约减后的SCADE模型的安全性质。

关键词： 面向对象测试   测试用例生成   UML   活动图   测试场景  

摘要： 测试用例作为软件测试的核心内容,是软件测试质量稳定的根本保障。基于UML模型的软件测试旨在通过将UML模型用于指导测试、验证模型与代码的一致性、检查软件产品是否符合需求和设计,提高软件测试质量。该方法的优点是可以重用开发、设计阶段的成果,加快测试用例生成。目前基于UML模型的测试用例生成方法主要有四种方式:基于形式规约的测试、基于图理论的测试、启发式测试和直接根据UML规格生成测试用例。每种方法对单一UML模型的讨论相对充分,而对多种UML图形的结合却鲜有涉及。另外,同开发设计过程相比,测试用例生成与具体实现、开发过程等多种因素相关,因此普遍存在着理性较强而实用性、自动化化程度差的现状。在分析UML动态模型的可测性基础上,本文将UML与统一软件开发过程相结合,针对系统级测试用例,提出了一种两级测试场景生成算法。算法以用例图为指导,首先对活动图进行语义扩充和形式化定义,在明确测试充分性准则的前提下将活动图转换为有向图,采用分支回溯深度优先遍历算法生成初级测试场景;其次,分别对图中的循环、并发模块进行迭代限定和内部活动进行排序生成二级测试场景;针对活动图内部活动排序提出并对比了三种可选方案:深度优先搜索、随机过滤生成和反蚁群算法;然后,根据乘法原理将两级测试场景组合,并对生成的测试场景按权值进行倒叙优化;最后,结合测试数据生成策略生成最终的测试用例。本文重点解决了活动图向有向图自动转换和并发模块引起的组合状态爆炸两个关键问题。本文提出的测试用例生成算法侧重于UML的实际工程实践,在铁路综合视频实时监控系统的应用中,生成的测试用例易用、准确,有效加快了系统测试的进程,验证了本方案的可行性和用于软件测试过程中的指导意义。

关键词： 道路桥梁   结构化   设计  

摘要： 在道路桥梁中结构化设计主要的操作方式就是把工程设计分为具有单一功能且相互独立的模块结构，包括概要设计和详细设计，希望通过结构图来描述设计阶段的诸多问题。结构化设计秉承了道路桥梁设计中的安全、适用和经济的基本原则，可以有效解决传统设计方法中存在的问题，有着广泛的应用前景。基于此，实际工作中对其应用有效性的研究探讨是很有必要的。

关键词： 列车运行平台   Matlab   仿真系统   分布式结构   UML建模  

摘要： 摘要：为了保证列车运行的安全、快速,需要利用更加有效、稳定的控制算法对列车运行过程进行控制,但想要在实际运行线路中进行列车控制系统的研究,显然是很不安全和很不经济的。所以,利用仿真技术搭建的仿真平台对列车运行中控制算法的研究和开发有着十分重要的意义。仿真平台的优势主要体现在两点：(1)仿真平台能更加经济、更加安全对列车运行控制算法进行评估和测试。(2)仿真平台可以方便展示列车运行的全过程,研究人员可以更加直观的了解列车运行控制算法的作用效果。 本文主要介绍了计算机仿真技术的基础上,研究了列车运行仿真平台软件的建模方法——采用统一建模语言(UML)进行模型建立,构建了列车运行系统软件的类图、用例图、时序图等,给出了整个仿真平台系统的运行流程图。通过对系统流程的分析,总结出仿真系统的四个模块包括仿真模型设置模块,网络传输模块,仿真程序计算模块,数据处理运行回放模块。然后运用C#.NET集成编程环境、Matlab开发环境和Access2010 数据库,同时利用模块化的程序设计方式对四个模块进行程序设计。 最后,利用列车自动驾驶算法,对仿真平台软件进行了仿真分析,验证了仿真平台的有效性。

关键词： 常山华侨经济开发区   办公管理系统   面向对象   UML建模  

摘要： 漳州市常山华侨经济开发区成立较晚,信息化建设进度相对滞后,研究开发区办公管理系统的开发,有重要现实意义。 论文介绍了漳州市常山华侨经济开发区办公管理系统的研究背景、项目意义和目前的研究与应用现状,明确了论文研究的内容和主要工作；论文中使用面向对象的软件工程方法设计了系统,并使用UML进行建模。在业务分析中,论文对系统存在的问题、组织机构、原有业务流程等进行了分析,给出了改造后的业务流程；在功能分析中,论文通过用例分析和用例描述,明确了系统的功能,给出了系统的总体功能架构和各功能模块的结构,包括文档管理、收文管理、发文管理、电子签章管理、公车安排管理、会议室管理、统计查询、用户管理、日志管理、组织机构管理等功能模块；在数据分析中,论文对系统各功能的所需要处理的数据进行了分析,给出了实体类关系图和详细的类属性,设计了数据库表单结构；论文最后对所做的研究与分析工作进行了总结,并对进一步的工作进行了展望。

关键词： 数据管理   B/S架构   UML建模  

摘要： 在信息技术越来越发达的今天,通过信息系统对企业的业务流程进行管理已经成为时代的要求,而在气体数据分析管理系统实现之前,主要由具体的人员负责进行管理,然后相关业务人员及时进专门的数据信息录入、数据审核及数据浏览操作等,这样的方法效率低下,耗时严重,需要较多的业务人员才能完成,严重增加了公司工作的成本,而且由于人为操作,导致经常时候出现错误,这样就造成业务数据信息管理混乱的局面,影响了数据管理的科学性与正确性,对公司效益的发展产生不利的影响本课题的主要目标为应用计算机技术来设计和实现更加满足当前系统对气体分析数据的存储。首先主要对本课题的项目背景、研究对象及其国内外研究现状进行阐述,并结合自己的看法提出一些在项目设计与实现过程中应注意的方面;然后针对本课题相关的技术概述,列出并简要的描述关键理论和技术在项目研究、设计与实现的过程中的作用;接着气体数据分析管理系统的需求分析。首先分析了气体数据分析管理系统具体的用户需求,然后对具体的需求进行建模,并给出系统非功能需求方面的内容,系统的核心部分主要关注了气体数据分析管理系统的设计方面的内容与实现的内容,着重根据系统的相关功能模块进行实现,从而从面向对象的观点进行具体的设计与实现;系统测试主要阐述了系统进行具体的内容,提供了系统测试的软硬件环境,设计合理的测试方案,提供测试用例来验证了气体数据分析管理系统的功能和有效性;最后总结与展望,对自己论文课题工作的总结,并对下一步的工作进行展望。另外对本系统的实际应用情况进行了总结,同时提出需要改进的几个方面。在气体数据分析管理系统进行开发完成后,通过具体的信息化管理方式,针对公司最重要的业务数据信息进行有效的管理,从而有效的拓展业务发展。在气体数据分析管理系统进行开发完成后,为公司业务的发展打造一个信息化的平台,通过这个平台,对系统进行设计与实现,可以对公司重要的业务数据进行有效的管理,减少工作业务成本,为公司的发展提供持续的动力,促进工作的全面提升。

关键词： 柳州职业技术学院   成绩管理   信息系统   需求分析   UML建模   数据建模  

摘要： 论文阐述了柳州职业技术学院学生成绩管理系统的分析与研究的背景,列出了需要解决的问题,说明了项目的意义与必要性。对于系统开发的方法和相关技术做了详细说明；重点分析研究了针对学生、教师、教务、院系功能模块的业务,具体包括考试管理、成绩登记管理、缓考管理、重修管理、学生基本信息管理、课程基本信息管理、系统管理八个子模块的详细分析。对其原有的业务流程进行了分析,并且进行了业务流程改造。论文针对系统的目标,分别对业务、功能、数据需求进行分析,展示了其业务流程图、用例图、包图和概念类图,以及用例说明；对于系统的数据分析,给出了e-r图以及数据库表设计。

关键词： 信息系统   面向对象法   UML建模  

摘要： 随着高校办学规模的扩大和招生人数的增加,学生成绩管理维护是学校管理中异常重要的一个环节,作为学校,除了育人,就是育知,学生成绩管理的计算机化是整个学校教务管理中的重要一部分,介于它的重要性,学生成绩管理系统的开发与应用就逐渐提入议程,并占着越来越重要的份量。运用学生成绩管理维护系统可以减轻学院教学人员的工作量,缩小开支,提高工作效率与准确率,能够节省时间,学生也能够尽快的知道自己的考试成绩,投入新的课程的学习或复习这次没有考过的课程。 论文介绍了学生成绩管理系统的研究背景、项目意义和目前的研究与应用现状,明确了论文研究的内容和主要工作；在业务分析中,论文对系统存在的问题、组织机构、原有业务流程等进行了分析,给出了改造后的业务流程；在功能分析中,论文通过用例分析和用例描述,明确了系统的功能,给出了系统的总体功能包图和子功能包图,包括用户管理、基本信息设置和成绩录入等子包图；在数据分析中,论文对系统各功能的所需要处理的数据进行了分析,给出了实体类关系图,建立了数据库表结构；论文最后对所做的研究与分析工作进行了总结,并对进一步的工作进行了展望。

关键词： 东莞   污染源监测   管理系统   研究与分析   UML建模  

摘要： 近几年来,东莞市政府开始重视起本市在环境保护方面的工作。但是伴随着经济和工业化的发展,东莞市管辖区域内的企业不断增加,污染源也越来越多。开始出现了污染源监测数据不断增加的现象,增加了污染源监测数据的管理工作的难度。东莞市环保局的工作压力也随之增大,随着全球互联网科技的崛起和计算机技术开始得到广泛的应用,建立健全一个合理有效的污染源数据管理系统,对于提高快速发展的科技信息技术在管理污染源监测数据过程中的运用,具有极其重要的意义。 首先,论文对东莞市的污染源监测管理系统这一课题的背景进行了大致的介绍,描述了论文中需要进行解决的问题,对本课题的研究目的和意义,论文中使用的建模工具等进行了讨论,并分析了本人主要的工作内容和论文的主要设计目的。以现有的污染源监测管理系统为根本,优化了业务流程中的部分环节,并且通过UML建模工具,开发了污染源管理、监测采集管理、超标报警管理、环境监理管理等系统主要活动流程,具体工作内容大致为：在业务分析中,论文对系统需要解决的问题、主要组织机构、原有的业务流程等进行了分析和概述,给出了再造后的业务流程；然后在功能分析中,论文通过用例图对系统各功能的用例进行了分析与描述,设计了系统的主要功能,通过系统的总体功能模块的包图和子功能模块的包图,对系统的各功能进行了总结；在数据分析中,论文在功能分析的基础上对系统的主要数据进行了分析,对各数据间的实体类关系进行了明确,建立了数据库表结构；在最后的总结中对本人的主要工作进行了阐述,指出了论文中出现的问题,并对将来的工作做出了美好的展望。

关键词： 自动化生产线   PLC   形式化方法   Event-B  

摘要： 自动化生产线是现代产品生产过程中一种控制系统,具有工作效率高,加工质量好,生产成本低的特点。自动化生产线通常由各种机械和电控设备组成,功能可以几乎包含了生产工艺的各个环节,使得它具有较高集成度,并且具有较高的自动化水平,可以有效减少人工操作,这些特点决定了设计的自动化生产线应具有较高的可靠性。在生产线正式投入工作前,要经过长期、大量的测试,用来发现程序中的错误,验证控制程序的正确性。但在实际情况中,有些错误可能由于测试时间和方法的不足,并没有通过测试检测出来;还有一些错误状况,由于现场条件的限制,无法制造条件进行测试。为了解决这一类问题,形式化方法应运而生。形式化方法通过数学的方法,对实际系统进行数学建模和验证,可以在不经过测试的条件下对系统进行验证,提高系统的可靠性,有效地降低了测试成本,适用于对可靠性要求高的场合。本文的内容是125I自动化生产线设计和可靠性验证,主要包括对生产线的结构、功能及相关控制技术的介绍,并且详细说明了PLC控制系统的设计方法。除此之外,由于125I生产线用于生产放射性药物,对控制程序有着较高的可靠性要求。因此,除了对生产线控制程序进行了常规的仿真和测试外,还对所设计的控制程序探究性地进行了Event-B形式化建模和验证,并介绍了相关的形式化方法原理,详细说明了Event-B方法的建模和验证过程。