教学课程资源库 更多>>

关键词： 形式化方法   Event-B方法   免疫模型   Rodin平台  

摘要： 在当今互联网时代,社会信息化飞速发展,大部分行业都不断提高信息化水平。在准备开发一个软件时,根据软件工程的思路需要对系统的需求进行分析,弄清楚目标系统必须做什么的问题。然而分析的过程中不可避免的存在矛盾、二义性、不完整性和抽象层次混乱等问题。形式化方法是通过系统的数学规格说明来保证需求无二义性,并且可以通过数学的方法进行验证,来查找系统中的矛盾和不完整性,以此来保证规格说明的正确性。常见的形式化方法有B方法和Event-B方法,本文通过形式化方法Event-B对免疫系统进行开发模拟,采用Rodin工具建立免疫系统模型,从需求重写、模型多次精化到模型中义务证明的验证,在软件开发过程中安全平滑地过渡到程序设计与编码阶段,保证软件开发前期的正确性与一致性。免疫系统的学习与研究可以加深对生物体中的机制的认识,免疫系统也可以对网络安全中的入侵、分布式中的一致性问题等提供思路。本文以免疫系统作为需求,采用Event-B形式化方法建立免疫系统模型,并在Rodin平台下对该模型从需求分析到模型验证,通过结合UML和Swing技术将系统开发完成,具体开展了如下工作:第一,阐述免疫系统中的免疫机制。根据Event-B形式化方法的建模过程,首先创建免疫系统初代抽象免疫系统模型,之后根据每一层细胞的特性进行精化,第一次精化引入了细胞生长的概念,第二次精化引入了免疫应答机制的概念,第三次精化引入了记忆细胞的二次免疫应答的概念,通过多次逐步精化的方式不断细化模型,使得模型符合生物学中的免疫系统。第二,研究Rodin中的证明规则、证明策略和证明类型等一些规则和方法,结合免疫系统模型逐层进行。通过Rodin证明了大部分证明义务,部分未完成的证明通过手动证明完成整个免疫系统的验证。第三,通过结合UML和Swing技术分析精化验证后的免疫系统模型,精化验证后的模型没有语义的二义性等错误。通过软件工程的思想进行详细设计,使用Java编程语言进行编写工作,实现了带有图形界面的免疫系统模型,可视化模拟病毒入侵到抗体对抗的过程,并实时统计不同时期细胞的数量的关系。实验运行结果得到与生物学免疫应答规律一致的结果,可供相关的免疫系统研究学习人员模拟教学使用。总而言之,通过形式化方法的流程去对免疫系统的需求进行精化验证,将精化验证后的模型结合UML和Swing技术进行实现,通过设置的相应细胞的参数进行模拟,发现其结果与生物学中的规律基本保持一致,验证了系统的合理性和可使用性。

关键词： 基于模型的设计   形式化方法   平台适配层   车站联锁  

摘要： 铁路安全控制系统是以技术手段控制列车运行方向、运行间隔、运行速度的安全关键系统。车站联锁是控制列车站内运行的铁路安全控制系统地面核心子系统。根据铁路安全控制软件行业标准EN50128,车站联锁必须具有最高安全完整性等级SIL4级。由于各个国家具有不同的技术标准,甚至不同站场都会有不同的用户需求,极高的安全性要求、多变的技术标准、多样的需求变化以及联锁内部的复杂控制逻辑对联锁软件的开发造成了极大压力。传统的开发方式使用自然语言和图形描述系统的需求和设计,使用人工进行分析、审查、测试保证系统满足功能和安全的要求,但设计中容易引入歧义和错误,开发和测试低效、修改成本高。基于模型的形式化方法能够有效解决传统的开发方式中的问题:采用形式化语言精确地定义系统行为,避免歧义;形式化验证方便检查系统安全性;采用基于模型的开发方式能够更清晰地描述系统,进行更早和更有效的验证;自动生成代码增加开发效率,减少人工引入错误。SCADE作为基于模型的形式化开发代表工具已被广泛应用于各安全控制领域的系统开发中。本项目的目标是使用SCADE工具进行通用联锁软件的研制。为了重构既有联锁软件,开发通用的、模块化的、可扩展的软件架构,将联锁软件划分为与具体的输入和输出相关的平台适配层软件和完全的联锁运算核心逻辑。本文就使用SCADE工具进行通用联锁软件平台适配层的设计和实现展开工作。本文按照SCADE软件开发流程进行平台适配层的需求分析和概要设计;使用SCADE模型实现联锁软件中与具体的硬件平台和通信相关的数据处理、通信协议、通信方式、安全冗余等平台适配层逻辑;实现通用的、适应变更的联锁核心逻辑接口;搭建起方便易用的模型仿真和生成代码的集成测试环境;最后在安全计算机硬件平台上验证平台适配层的可行性,为SCADE开发联锁软件平台适配层提供一套可行的解决方案。

关键词： 桥梁结构化设计   价值   应用措施  

摘要： 伴随着社会经济的不断发展,我国当前桥梁工程设计水平也不断进步和发展,在众多桥梁设计提升质量水平过程中,其结构优化设计总体成效更为显著,该优化设计技术也是当代桥梁设计工程施工的主要核心技术之一。鉴于此,本文重点针对当前桥梁结构工程设计的基本机制和应用优化措施进行了分析和探讨,以供借鉴。

关键词： 校企合作   软件工程   实践教学   人才培养   教学改革  

摘要： 近几年来计算机类校企合作专业在很多省都已开设,本文以临沂大学软件工程校企合作专业为例探讨了软件工程校企合作实践教学体系的构建与实践,研究了校企合作模式下实践教学体系的制定、突出实践能力的教学模式、校企共建实训基地、四层递进实践教学内容体系的设置以及实践教学体系运行机制,该实践体系提高了学生的实践创新能力,同时为同类院校软件工程专业校企合作的共建模式提供借鉴.

关键词： 矿井气体监测   WSN系统架构   UML建模   Java Web   可燃气体浓度  

摘要： 近年来,随着我国科技的快速发展和企业安全意识的不断提高,瓦斯气体事故造成的人员伤亡逐年下降,但其灾难性后果依然不可轻视。在实际生产过程中,大多数企业现有的矿井气体检测系统已难以满足企业和一线工人日益增长的需求。因此,项目组设计并实现了矿井气体监测与预警系统。该系统既满足了鹤壁市德政气体检测有限公司优化升级的具体要求,也可以服务于其他相关企业。作为矿井气体监测与预警系统的重要组成部分之一,本文设计和实现的软件服务子系统包括信息监测子系统、预警信息子系统、设备校验子系统和后台管理子系统四部分,可实现瓦斯气体的实时数据监测、历史检测数据查看、历史报警数据查看、实时预警数据查看、图表展示和设备校验等功能。本文主要工作如下:(1)需求分析阶段:通过现场实地调研和与现场会谈等方式与鹤壁市德政气体检测有限公司的相关技术人员进行交流沟通,与项目需求结合,使用UML中的用例图、领域模型和系统顺序图明确系统需求,建立需求分析模型。(2)概要设计阶段:设计完成系统的网络拓扑图、系统结构模型和数据库物理结构,建立系统核心架构;详细设计阶段,通过使用类图、时序图和流程图对项目的业务逻辑进行详细的描述,最终使用Java Web开发技术进行实现。(3)针对瓦斯气体预警这个关键问题,充分调研,提出了解决方案并进行了完整实现。为满足不同预警等级相应的对策要求,系统中提供三种预警模式——稳定模式、扰动模式和聚集模式;并根据其判别标准建立和实现三种等级的预警——安全、关注和紧急。矿井气体监测与预警软件服务子系统已经通过鹤壁市德政气体检测有限公司的验收测试。验收结果表明该系统能充分满足用户系统软件方面的需求。在矿井气体监测与预警系统的基础硬件环境部署完毕后,软件服务子系统可以顺利进行部署和试运行。

关键词： 新冠状病毒   软件工程   网页设计   教学改革   DIV+CSS  

摘要： 在互联网技术迅猛发展的时代,网络已经成为人们生活中很重要的一部分,作为服务于社会经济发展的高校专业设置,为适应时代需求,软件工程专业开设了网页设计课程。网页设计是软件工程专业的一门专业基础课,该课程教学内容从实践出发,注重培养学生静态网页制作方面的使用技能和应用能力,掌握静态网站的建设、使用和管理能力。本文重点探讨软件工程专业网页设计课程的教学改革实践,针对网页设计课程教学开展了不同形式的教学改革,培养学生的知识迁移能力,促进学生的实际应用能力,增强学生的自学意识和自律能力,不畏困难,勇于创新,取得了良好的效果。

关键词： 光谱仪   软件开发   组合滤波   寻峰算法   定标算法   UML建模  

摘要： 随着集成电路、光电传感器制造工艺以及计算机技术的迅速发展,一种基于CCD探测器的微型光纤光谱仪应运而生来满足环境、农业科技、生物医学等各领域对光谱分析的应用需求。为充分发挥光谱仪设备的硬件性能,扩展其应用范围和实用性,同时也是出于仪器智能化和提升光谱数据质量的目的,本文在研究光谱仪系统的结构和工作流程、光谱数据的传输过程以及数据处理算法的基础上,设计并实现了光纤光谱仪数据接收与处理多功能应用软件。首先,本文从光纤光谱仪整体系统结构设计入手,研究CCD的光电转换原理及基本特性为后续数据预处理算法的设计和软件采集控制程序的开发奠定理论基础;学习软件系统的设计思想,根据瀑布开发模型展开面向对象的软件开发。其次,本文针对光谱数据噪声特点,在研究Savitzky-Golay卷积滤波法和中值滤波法的基础上提出了SG—中值组合滤波的方法,测试结果表明该方法在剔除异常值的同时也能有效地抑制高斯白噪声。为完成波长定标工作,本文设计了一种基于阈值参数导数寻峰算法与最小二乘多项式拟合法相融合的定标算法。实验数据表明采用3阶多项式拟合能够在满足数据实时性的前提下将偏差控制在较小范围内,并验证了在整个响应波长范围内均匀选取拟合特征峰位可得到更准确的定标结果。最后,本文在对光谱仪软件需求分析的基础上,根据面向对象的软件思想,利用UML建模语言进行软件设计,在基于C#语言的Winform桌面应用程序框架上,运用模块化的方式设计实现了一款光谱仪数据接收与处理多功能软件,通过VCP通信、WMI信息管理、多线程、乒乓缓存和自定义控件等技术完成了软件各模块的开发工作。本软件完成了与光谱仪设备之间的通信,实现了软件对硬件的控制,可选用多种采集方式,能够稳定接收来自下位机的光谱数据,对数据进行背景扣除、平滑降噪、模式计算、寻峰剪峰等处理,并在界面以光谱视图或时序视图实时显示,还为谱线分析和数据操作提供了丰富的辅助功能。系统测试结果表明,该软件能够保证数据的安全性,且具备良好的稳定性和实用性。

关键词： 形式化方法   自动化验证   Isabelle定理证明器   深度优先搜索算法  

摘要： 形式化方法以严格的数学化和机械化方法为基础来规约、构建和验证计算系统,是改善和确保计算系统质量的重要方法,其模型、技术和工具已延伸成为计算思维的重要载体。形式化方法中,形式化推导是通过对问题程序规约进行精确变换,最终得到算法程序。形式化验证是在对软件进行规约的基础上,验证软件是否具有所期望的性质。软件形式化方法使软件系统的描述更加精确,以减少可能的错误所带来的问题,提高软件的可靠性。图结构在现实生活中应用非常广泛,图的数据结构广泛应用在公路运输网络、地铁线路网络、网络节点优化等生活中的很多领域,另外计算机系统中的状态执行等也是基于图数据结构的。因此,图的深度优先遍历算法在现代的各种软件中应用十分频繁,这些软件的可靠性的高低很大程度取决于图的深度优先算法是否正确完备。深度优先算法的可靠性验证使用传统的手工推导来验证已经不能满足我们的需要了,数学定理证明工具Isabelle与软件形式化方法的结合既可以适应日益繁琐的软件验证,又可以避免手工推导验证所带来的失误。Isabelle是一种通用的且支持高阶逻辑的交互式定理证明器。它允许以正式语言表达数学公式,并提供用于在逻辑演算中证明这些公式的工具。主要应用是数学证明的形式化,尤其是形式化验证,其中包括证明计算机硬件或软件的正确性以及证明计算机语言和协议的特性。本文研究的内容主要是深入了解Isabelle系统的验证原理和逻辑结构,探索将形式化方法与Isabelle定理证明器相结合应用于实际生产,在对比形式化方法中的几种验证方法的优缺点后,选择使用Dijkstra最弱前置谓词方法作为验证方法。为了实现对深度优先遍历算法的验证,本文对Isabelle系统的规则库中加入了图的定义、深度优先遍历算法及其相关引理。并且结合Dijkstra最弱前置谓词方法完成了对图的深度优先遍历算法进行自动化验证。这些工作确保了深度优先遍历算法的可靠性和简化了手工推导验证的繁琐程度。扩充的Isabelle类型库为以后的研究者丰富了图结构的定义。将形式化方法与证明工具相结合一定程度上会促进形式化方法应用到实际生产中。

ISBN: (纸本)9787121376276

关键词： 道路桥梁设计   结构化设计   应用研究  

摘要： 随着我国经济的高速发展,交通建设领域也得到了快速的提高。道路桥梁设计是交通建设行业重要的组成部分,本文主要分析探讨结构化设计在道路桥梁设计中发挥的重要作用及结构化设计在道路桥梁设计中的具体应用。