教学课程资源库 更多>>

关键词： 分区操作系统   组合形式化方法   定理证明   模型检测  

摘要： 综合模块化航空电子系统已被广泛应用于航空、航天等安全关键领域,其主要目标是实现分区操作系统,为多个安全级别的子系统提供资源共享的运行平台,并采用时间隔离和空间隔离机制保证应用程序之间的故障隔离和信息流控制。由于分区操作系统的复杂性,其安全性和可靠性往往难以通过测试和仿真手段来保证。需要采用严格的形式化方法,建立清晰的、无二义的数学模型,并采用数学推理和验证的手段来保证其时间隔离能力和空间隔离能力。当前对分区操作系统的建模及验证工作主要包括采用定理证明方法来验证其空间隔离属性或采用模型检测方法来验证其时间隔离属性,缺乏一个统一的框架来完整地解决时间和空间隔离属性的形式化建模及验证工作。这主要是由于定理证明类的建模语言通常无法建模系统的控制流和时间,也无法表达并发对象的交互行为。反之,模型检测方法所使用的工具和语言通常都缺乏良好的逐步精化框架,对数据密集型的系统的建模和验证能力也存在不足。本文以分区操作系统的建模及验证需求为牵引,针对定理证明类建模语言Event-B和模型检测方法LTS以及时间自动机的缺点,提出了一种组合形式化方法,给出了一个基于组合形式化方法的分区操作系统建模及验证框架,构建了Event-B的行为语义模型和时间语义模型。在此基础上,完成了分区操作系统的行为属性和时间属性的建模及验证。所完成的工作和创新点主要体现在以下几个方面:(1)研究了Event-B建模语言和模型检测类的形式化建模语言的组合建模问题,提出了一个基于组合形式化方法的分区操作系统建模及验证框架。本文针对Event-B和LTS、时间自动机等方法的局限,提出了一种“相互表示”的方法,用Event-B状态机来表示LTS和时间自动机的建模元素。在此基础上,提出了一个组合Event-B和LTS以及时间自动机的系统建模及验证框架,为组合使用多种形式化方法完成复杂系统建模及验证提供了一种新的思路。(2)研究了Event-B建模语言的行为语义模型和时间语义模型,并完成了这些语义模型的正确性证明。本文针对Event-B建模语言缺乏行为语义和时间语义的局限,使用LTS表达Event-B的行为语义,并使用时间自动机表示Event-B的时间语义;给出了从Event-B模型到LTS模型及时间自动机模型的转换规则,并采用LTS之间的互模拟等价关系证明了Event-B模型和其对应的行为语义模型及时间语义模型的行为等价性,为组合使用Event-B建模语言和LTS及时间自动机完成分区操作系统建模和验证奠定了理论基础。(3)研究了LTS和时间自动机等模型检测类建模语言的逐步精化方法,并给出了一个逐步精化框架。传统的模型检测类建模语言通常都缺乏从抽象模型到具体模型的逐步精化框架,给系统建模和分析工作带来很大的困难。本文针对这一弊端,借鉴了Event-B的逐步精化过程,提出了LTS和时间自动机模型的逐步精化框架,将模型的演化过程归纳为在垂直方向上对某个对象的行为的分解以及在水平方向上逐步引入更多的并发对象,并给出了各种垂直精化模式和水平扩展模式,为开发多视图的组合形式化模型提供了新的思路。(4)在上述工作的基础上,构建了分区操作系统的行为模型及时间模型,完成了分区操作系统的行为属性验证和可调度性验证。在前述工作的基础上,本文首先使用定理证明语言Event-B构建了分区操作系统规范ARINC 653的模型,并将其转换为等价的LTS模型,通过验证LTS模型的行为属性保证了Event-B模型的相应属性。而后,使用Event-B搭建了分区操作系统的两级调度模型,并将其转换为对应的时间自动机模型;通过验证时间自动机模型的可调度性保证了Event-B模型的可调度性。通过以上两个模型的构建和验证,证明了本文所提出的组合形式化方法的实用性。

关键词： MOOC   移动SPOC   翻转课堂  

摘要： 移动互联网的飞速发展,促进了翻转课堂的改革。本研究在《软件工程导论》课程中实施基于MOOC+移动SPOC的翻转课堂实践,结合课程特点,制定任务驱动的项目教学,给出具体的实施方案和实施过程,以期对其他相关课程的教学起到借鉴作用。

关键词： 安全关键系统   安全性验证   模型驱动   需求可追踪性   形式化方法  

摘要： 安全关键系统广泛应用于各种行业领域,例如国家的航空航天项目以及近年来迅速发展的无人驾驶、智慧医疗等领域。该类系统对安全性有着极高要求,一旦出现系统失效即可能造成重大的生命财产损失,因此,如何保障该类系统的安全性一直是学术界以及工业界的重要议题。安全性需求描述了系统不应发生的危险状态,来源于系统的早期危害分析以及后续的安全性分析迭代,尽早对其验证可以有效提高系统安全性。然而,在实际的系统开发过程中,系统设计模型基于功能需求进行开发,这导致了安全性需求与系统设计之间存在沟壑,使得设计模型是否满足安全性需求难以验证,系统的安全性难以得到有效的保障。针对以上问题,本文提出了一种基于SysML面向安全关键系统的安全性需求追踪及验证方法。本文主要研究内容如下:首先,参照相关安全标准,提出一个面向安全关键系统的追踪信息模型用于指导建模中追踪信息的捕获;接着,针对标准SysML需求图缺乏描述安全性需求能力,本文对SysML需求图进行了扩展,使其可以建模安全性需求并捕获追踪信息;此外,针对SysML需求图缺乏安全性需求追踪信息的导出机制,文中通过模型转换将需求图转换到追踪信息表达模型,生成独立的追踪信息文档,为后续安全性验证提供直接支持。其次,利用追踪信息定位SysML设计模型中用于实现安全性需求的SysML块以及块中元素,根据定位到的安全关键SysML设计给出算法构建面向验证的SysML块定义图进行安全性验证;但由于SysML模型缺乏精确语义,难以直接进行验证,故而本文中接着给出了从SysML模型转换到NuSMV形式化模型的规则,将SysML块定义图和状态机图转换到可验证的NuSMV系统模型,通过模型检测器验证安全性需求满足情况。最后,使用本文的方法对一个铁路控制系统进行案例分析。通过验证发现了系统设计中存在的缺陷,有效识别了潜在风险,同时也说明了本文方法的有效性。本文方法提供了一种安全关键系统中可追踪性建立以及利用追踪信息在系统开发早期定位系统安全关键组件并验证安全性的可行思路。

关键词： 搪瓷喷涂工艺   培训考核   Spring MVC技术   UML建模  

摘要： 微波炉搪瓷制作是非常复杂的一种工艺,这种复合材料生产过程会因为受到不同外部因素的影响而导致产品质量差异,其中搪瓷喷涂工艺是其中非常关键的工序,被企业高度重视,并组织相关技术培训来提高员工的掌握水平。传统的培训方式组织难度大、培训任务大,而且耗费大量人力物力,培训工作管理效率低下,培训资源利用率和共享程度不高,缺乏高效、准确的统计手段,不能为培训工作的开展、培训内容的合理选择提供科学依据。同时培训效率低下,培训效果无法考核,因此,亟需通过开发一套信息化的培训考核软件来解决问题。本文首先提出了课题建设的现实背景,对国内外相关研究进行了阐述,明确了论文研究主要目标和重要意义,介绍了论文的主要工作与组织结构;然后对系统开发过程应用的核心技术的构成、工作原理以及技术特点进行阐述,主要包括Spring MVC、MyBatis、Oralce、Jquery、Tomcat等技术;其次分析了系统构建的可行性,指出了系统主要用户构成,对系统业务功能、业务流程等进行了需求分析,指出了系统非功能性需求;再次对系统进行详细设计,明确了系统设计需要遵循的相关原则,采用层次化方式设计系统应用架构,主要包括用户层、表现层、业务功能层、数据访问层、数据存储层,相邻层次相互作用,下层为上层提供数据或者业务服务,然后采用流行Spring轻量级框架设计系统技术架构,确定系统部署环境,搭建系统网络架构,确定系统采用的各种技术、架构内容,培训考核管理系统使用UML建模语言构建,主要包括系统登录、资源管理、培训管理、考核管理、资讯管理、统计分析、基础信息管理、系统管理等功能模块;最后进行了系统性能、功能、数据等方面测试,测试表明系统功能正常、性能稳定,能够发布上线。本课题设计完成的搪瓷喷涂参数培训软件,促进了企业向学习型组织的转变,为企业培养更多有市场竞争力的学员,提升了公司产品创新能力和研发水平。同时提高了企业员工搪瓷生产水平与工作效率,加强了研发与市场的沟通交流,缩短产品进入市场的时间。通过对员工进行培训,增强了企业的凝聚力,提高了员工的忠诚度,使学习成为一项关键业务,提高了部门间的协作和交互能力。

关键词： 民航   飞机维修定检   系统设计   UML建模  

摘要： 随着高科技行业的白热化发展趋势,我国已经进入高科技信息时代,高科技在日常生活中的运用很大程度上给人们的生活带来了便利。在民航行业中,飞机维修定检是一项重要的问题,所以对于任何航空公司来说,飞机维修定检是保障航班顺利进行的基础条件,所以加强飞机维修定检的管理是航空公司或者机场的重点工作。一般情况下飞机维修定检管理不善是影响航空公司发展的一个重要因素,民航飞机维修定检管理中定检维修产生的各种信息的传递、处理的效率,是影响民航定检维修管理效果的关键因素。实现飞机维修定检信息化服务是指将飞机维护通过信息化平台实现资源共享,让飞机维修定检管理更规范化。近几年随着经济的发展,人们对航空飞机的需也越来越大,为了适应航空需求,航空市场迅速壮大,国内投入到航空市场的飞机越来越多,在很大程度上带动了航空业的发展,随之也带动了机修业的崛起。而航空业的发展的投入成本也随之增大,据不完全统计,近年来的机修成本就高达总投入的百分之二十,数目巨大的背后也带来了巨大的压力。而对航空飞机进行实时的检修和日常的护理也是为了让飞机保障其运行的安全。因此,设计一款管理飞机维修定检管理系统就显得较为重要。本文主要分析了基于SAP模式的飞机维修定检系统。首先,文章在对国内外飞机维修定系统研究相关检理方面研究的基础上,根据飞机定检维修的具体情况,选择适合航空飞机的定检相关的SAP方案,也就是从指令到流程的模式。然后,通过SAP方案的服务和UML的有机结合,来制定详细的飞机维修定检理的具体方案设计,再次,本文通过多元化的角度出发,根据具体的需求,运用图文的形式对SAP飞机维修定检系统进行具体的分析;将SAP飞机维修定检系统技术要点与UML进行结合;最后对SAP飞机维修定检系统设计做相关的检测。从系统功能包括:定检计划管理、维修指令管理、维修代理协议管理、维修流程管理、维修设备管理、系统配置管理。通过对功能点分析,该系统的应用将做到飞机维修定检理的各个方面,实现对程定检维修的科学管理,以帮助民航企业更好的进行飞机维修定检程管理。同时通过测试表明,该系统既能有效地减少内部因信息处理延和信息丢失导致的资源的浪费,能在很大程度上节约资源,通过对飞机维修定检系统的优化,在很大程度上迎合了航空业的发展初衷。

关键词： Huisgen反应   含能材料   聚叠氮缩水甘油醚   网络结构  

摘要： 聚合物粘合剂作为固体推进剂的弹性基体,是决定固体推进剂力学性能的关键组分。大多数热固性粘合剂体系都采用异氰酸酯固化,但是由于异氰酸酯对湿度的敏感性,容易形成有缺陷的网络结构,对含能药柱的机械性能产生不利影响,而且在高能硝酸酯增塑剂推进剂体系中,异氰酸酯也可能导致不必要的亚硝基衍生物的形成,不利于固体推进剂的保存。发展高力学性能,且对环境湿度不敏感,能与含能颗粒组分相兼容的热固性粘合剂体系,成为含能材料发展的技术需求。作为一种典型的点击化学反应,叠氮基与炔基的Huisgen环加成反应备受复合材料领域研究者的重视。炔基与叠氮基通过Huisgen环加成反应制备的三唑环的过程,具有对水不敏感、反应效率高、条件温和、无其他副产物等优点,能构建新的三唑固化体系。值得注意的是,面向含能材料高能化和绿色化的发展趋势,备受关注的叠氮聚醚类含能粘合剂不但能与高能硝酸酯类增塑剂具有良好的相融性,侧链上丰富的叠氮基能完美的适配三唑固化体系。本课题中,针对Huisgen反应的非水敏感三唑固化体系,分别从炔基化化合物的官能度数目、颗粒固化协同剂和类聚氨酯结构的设计上出发,探究决定三唑固化体系高力学性能的关键因素与设计准则,期望得到粘合剂基体的高性能化及调控方法。本研究首先选取了分子链段柔顺型优良的炔基封端的四氢呋喃与环氧乙烷的共聚物(PPET),与聚叠氮缩水甘油醚(GAP)构建三唑网络,通过调控叠氮基与炔基的摩尔比的策略,对比两炔基官能度的p-PPET和三官能度的t-PPET构建的网络性能与结构上的区别。两者的交联密度都呈现着随着叠氮基与炔基的比值增加先上升后下降的趋势,同时t-PPET构建的三唑网络在相同反应基团的摩尔比下具有更高的交联密度,说明多炔基官能度的大分子由于其更加立体的结构,有助于网络的构成。力学测试表明,随着叠氮基的比例增加,网络的力学性能变化与其交联密度变化一致,t-PPET/GAP在叠氮基比炔基的比例为3时,拉伸强度、杨氏模量和断裂伸长率均取得最大值,分别为1.38MPa,4.07MPa和122.50%。多壁碳纳米管(MWCNT)也是常用于纳米改性增强的纳米颗粒,同时已有研究证明,MWCNT加入含能材料中可以促进燃烧分解。针对原始MWCNT在有机基体中分散性不好的缺点,以颗粒固化剂的思路出发,设计以炔基化MWCNT作为颗粒固化协同剂加入炔基封端的聚四氢呋喃(PTMO)与GAP的网络中,利用炔基化MWCNT和GAP之间形成三唑环,促进MWCNT在基体中的分散,构建共连续结构的模式,提升网络性能。测试结果表明,当炔基化MWCNT的加入量为1.0 wt%时,纳米复合材料的力学性能得到同步增强增韧,此时拉伸强度达到2.03MPa,杨氏模量和断裂伸长率相比空白样品分别增长了107.70%和23.56%。鉴于热固性粘合剂异氰酸酯固化体系体现的优良力学性能以及含能材料应用的验证,设计构建基于三唑固化体系的类氨酯结构的粘合剂体系,期望得到高伸长率和高模量的调节技术。利用TDI对具有优良柔性链段的羟基封端的四氢呋喃和环氧乙烷的共聚物(Poly(THF-co-EO))封端,再用丙炔醇反应得到具有异氰酸酯结构的炔基化合物,炔丙氧基羰基胺末端四氢呋喃/环氧乙烷共聚物(PrPET),然后与端叠氮封端的的聚醚(ATPET)构建固化网络。力学测试显示,ATPET/PrPET构建的网络,在反应官能度为1.0时,获得最佳的力学性能拉伸强度2.05MPa,模量1.88MPa,断裂伸长率221.40%。

关键词： 形式化方法   事件逻辑理论   移动支付协议   认证性   不可否认性  

摘要： 随着移动设备的迅速普及以及移动互联网的飞速发展,移动支付给人们的生活带来很大的便利。移动支付是实现移动电子商务交易成功的关键环节,安全的移动支付协议是保障移动支付顺利进行的基石。由于安全协议往往运行在复杂的、不安全的网络环境中,产生的错误很难发现,难以保证协议安全性分析的准确性,必须采用形式化方法和工具来分析。针对移动支付中存在的安全问题,对移动支付协议进行形式化分析,旨在发现移动支付协议中潜在的安全漏洞具有重要意义。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,可用于证明网络安全协议的安全性。本文基于事件逻辑理论并对其进行扩充,对移动支付协议进行形式化分析。本文主要研究内容如下:1.详细介绍事件逻辑理论的产生背景、发展现状、基本思想;对事件系统中的消息自动机和事件系统结构做了阐述,说明事件逻辑是如何去捕捉并描述一个分布式系统;给出事件逻辑理论中的基本定义,包括Atom原子、事件序、事件类,给出了事件逻辑证明系统中的六条公理以及相关引理及性质,其中着重对协议形式化建模中基于事件逻辑的协议建模逻辑与普通的消息-箭头描述方法进行了对比,突出了事件逻辑在协议建模方面的优势;总结归纳了基于事件逻辑的安全协议形式化证明流程图。2.针对移动支付协议中主体数目、协议交互步骤数目较多的情况下,提出迁移规则和可继承性,协议线程中的动作可以迁移到下一个序列中,对于多个协议主体数目、协议交互步骤数目多的协议,能够简化协议证明流程,有效减少协议证明的复杂性。通过事件逻辑理论分析移动支付协议KerNeeS协议安全性,对POS、NFC Phone和Authentication Server间交互进行分析。形式化描述协议双向认证过程、分析协议交互双方的基本序列,基于事件逻辑证明系统对强认证性质进行证明,得出POS和NFC Phone之间能够实现双向认证。3.针对事件逻辑只能分析安全协议认证性而不能分析不可否认性的缺陷,对事件逻辑理论进行扩展。增添了Has、CanProve、Claims、Controls等谓词,扩展协议证明系统,加入拥有公理、管辖公理、签名公理,让扩展的新方法能够对包含不可否认性的协议进行描述与分析。4.对不可否认性进行了定义与分析,使用事件逻辑对其进行形式化刻画说明,阐述了形式化分析不可否认性的具体步骤。首先列举协议的初始状态,包括协议的初始消息拥有集合和初始信念集合,对协议主体的初始状态集合进行了说明,并给出消息、信念的生成规则;接着列举发送方非否认证据EOO和接收方非否认证据EOR,分析EOO和EOR是否符合不可否认性要求;最后分析协议是否达到不可否认性目标,当协议运行在任何阶段时,是否有EOO∈和EOR∈同时成立,从而来分析协议的不可否认性是否满足。根据上述证明流程,以移动支付协议FMPP协议为例进行了形式化分析,说明了结果扩展的事件逻辑能够分析移动支付协议的不可否认性。

关键词： 软件工程   教学改革  

摘要： 新经济的发展对传统工程专业人才培养提出了挑战.相对于传统的工科人才,未来新兴产业和新经济需要的是工程实践能力强、创新能力强、具备国际竞争力的高素质复合型"新工科"人才,他们不仅在某一学科专业上学业精深,而且还应具有"学科交叉融合"的特征;他们不仅能运用所掌握的知识去解决现有的问题,也有能力学习新知识、新技术去解决未来发展出现的问题,对未来技术和产业起到引领作用.可以说,新经济对人才提出的新的目标定位与需求为"新工科"提供了契机,新经济的发展呼唤"新工科".目前,很多高校都已经开设软件工程专业,培养了大批软件工程专业人才.然而,新工科带来前所未有机遇的同时,也给现有的软件工程技术和软件工程专业教育带来一系列挑战.对此,文章主要基于新工科背景下,对《软件工程》课程教学改革方面进行详细分析,希望能给相关人士提供重要的参考价值.