导读:本文包含了形式化约束论文开题报告文献综述及选题提纲参考文献，主要关键词:移动ad,hoc网络,ZRP,SRP,Ariadne
形式化约束论文文献综述
付春艳[1]（2019）在《基于Event-B的ad hoc路由协议及任务级时间约束的形式化建模与验证》一文中研究指出移动ad hoc网络是由移动节点搭建的临时通信网络。网络中没有任何固定的基础设施和中心管理设备。因为节点可以自由移动,网络拓扑随时可能发生变化。所以ad hoc路由协议必须能在动态的环境中找到从源到目标的有效路径。这使得在此种网络中的路由选择比在有线网络中的路由选择更具有挑战性。当前研究人员已经提出许多在可信的网络环境下工作的ad hoc路由协议,可以分为叁类:主动式路由协议、反应式路由协议和混合路由协议。移动ad hoc网络中节点采用无线通信方式,并且没有固定基础设施和中心的安全控制。同固定网络相比,移动ad hoc网络更容易受到物理和通信攻击。此类网络的安全性越来越受到重视。基于在可信环境下工作的路由协议,研究人员提出在非可信环境下工作的安全ad hoc路由协议。如何保证研究人员提出的路由协议或算法的正确性成为一项具有挑战性的任务。本文对当前ad hoc路由协议形式化验证工作进行研究,总结采用Event-B方法从系统需求到形式化建模和验证的分析流程。此外,针对Event-B不支持时间属性描述的问题,提出了任务级时间约束模式。本文的主要贡献如下:·在可信的网络环境下,大多数研究者对单独的主动式路由协议或者反应式路由协议完成了形式化建模与分析。本文采用Event-B方法对混合路由协议ZRP进行建模与分析。本文对协议突出的方面进行了建模:网络拓扑的连接性;节点根据周期性交换的邻居信息构建路由区域;采用边界广播服务的路由发现过程;反应式模块的路由更新。利用Rodin工具,证明了模型构建过程中产生的证明义务,从而确保精化的正确性以及发现路径的无环性和有效性。此外,本文利用ProB对模型与需求描述的一致性进行了确认。因此证明了ZRP协议中路由发现机制的正确性。·在不可信的网络环境下,对安全按需源路由协议SRP的形式化建模与分析。首先,提出了正确发现路径的定义,作为判断协议是否正确的标准。然后根据系统假设和系统需求构建Event-B模型:环境模型,路由发现过程和攻击模型。环境模型考虑了网络拓扑的不稳定性。在攻击模型中考虑了节点丢弃攻击,创建循环路径和创建不存在路径叁种攻击行为。通过对不可证明的路径存在性的分析,得出该协议不能防止节点丢弃攻击和创建不存在路径攻击,并给出实例对这些情况进行说明。·在不可信的网络环境下,对安全按需源路由协议Ariadne的形式化建模与分析。由于攻击通常发生在特定的网络拓扑上,在模型构建时,假设网络环境是稳定的。因此,模型对于正确发现路径的存在性,以及网络环境的建模会与SRP协议构建的模型有所不同。模型中考虑了创建循环路径、创建不存在路径、节点删除攻击和虫洞攻击。通过对不可证明的路径存在性的分析,得出该协议不能防止创建不存在路径、节点删除攻击和虫洞攻击。最后,本文给出实例对这些情况进行说明。·针对Event-B不支持时间属性描述的问题,本文提出了任务级时间约束模式。采用Event-B构造用于描述重合、互斥、优先和子事件任务级时间约束的模式。首先构建描述单个任务时间属性的任务最后期限模式。在此模式基础上,通过精化机制构建不同的任务级时间约束模式。它们适用于实时系统的形式化建模和分析。最后,采用提出的重合和优先模式对实例进行形式化描述与分析。(本文来源于《浙江大学》期刊2019-01-10）
应云辉[2]（2018）在《基于SMT的时钟约束语言CCSL形式化分析与应用》一文中研究指出随着实时嵌入式系统在汽车和航空电子等领域的复杂性和安全性日益突出,应用严格分析技术以确保系统可预测就显得非常重要。因此统一建模语言UML采用了 MARTE(Modeling and Analysis of Real-Time and Embedded Systems)作为其在实时嵌入式系统领域的扩展,提供了规范、设计和验证平台的支持。MARTE提供了一个丰富的时间模型,当使用MARTE时间模型时,许多相互依赖的时钟要在模型中定义,而这种时钟的相互依赖关系可以由一门专用的语言指定,称之为时钟约束语言(CCSL)。CCSL指定了时钟间同步和异步的约束关系,为MARTE模型上的因果时序分析提供了支持。一个重要的问题是验证描述系统模型时间需求的CCSL约束的可满足性,这个问题能够帮助开发人员在系统设计阶段发现缺陷,从而避免在开发阶段带来不必要的损失。目前许多研究人员都在探寻CCSL的形式化分析方法,主要是利用迁移系统、Promela语言、Buchi自动机、时间自动机、重写逻辑等对CCSL约束进行转换,结合相应的工具进行分析验证。然而有些方法需要不寻常的中间转换过程,容易导致出错或者效率低下。有些转换方法不能转换所有的约束或者只考虑了部分约束的转换。基于状态的转换方法容易导致状态爆炸,影响分析效率。本文提出基于SMT的统一而高效的CCSL形式化分析方法,可用于CCSL的可调度分析、LTL模型检测、死锁检测、蕴含关系证明以及迹分析,依托于高效的SMT求解器Z3和CVC4进行分析和验证。将CCSL约束转换成SMT公式的过程是十分自然的,避免了复杂的中间转换过程,从而降低了出错的风险。不同于一些方法只能转换部分CCSL约束,CCSL约束到SMT公式的转换没有这个限制。众所周知,基于SMT的方法能够有效的克服模型检测的状态爆炸问题,利用该方法提升了对CCSL约束进行模型检测的效率。同时基于SMT的方法还能通过理论证明来证明CCSL约束具有一些属性,这是大部分现有的对于CCSL形式化分析方法缺少的。本文不仅交代了基于SMT的CCSL形式化分析方法在五个方面上的理论实现,而且给予相应的实际例子表明方法的可行性和有效性。自主开发了一个CCSL的分析验证工具,集成提出的方法,并应用了一个铁路联锁系统的案例。(本文来源于《华东师范大学》期刊2018-04-01）
应云辉,张民[3]（2018）在《基于SMT的时钟约束语言CCSL的形式化分析方法与工具》一文中研究指出时钟约束语言CCSL是一种用于描述实时嵌入式系统中事件之间约束的形式化语言,它是UML针对实时嵌入式系统建模的扩展包MARTE(modeling and analysis of real-time and embedded systems)中用于对时间建模的一个子语言.给定一组由CCSL定义的时钟约束条件,需要判断是否存在某种调度策略满足约束、是否所有满足这些约束的行为都不会导致系统死锁等分析.目前已经有一定的针对CCSL的形式化分析研究工作,如基于状态迁移系统与时间自动机的方法等.但这些方法要么只针对某种特定的分析,要么只适用于部分CCSL约束,要么分析效率较低.提出了基于SMT的统一且高效的CCSL形式化分析方法.统一性体现在其可用于有效性证明、迹分析、死锁检测、LTL模型检测等方面的验证与分析.基于该方法开发了原型工具,同时支持上述4种验证功能.工具集成了当前最高效的SMT求解器Z3和CVC4.得益于SMT求解器的高效性,实验中大部分的验证可以在短时间内完成.(本文来源于《软件学报》期刊2018年06期）
查欣欣[4]（2017）在《基于时间自动机的时序约束活动异常监测系统形式化验证》一文中研究指出物联网被认为是继计算机、互联网和移动通信网络之后的第叁次信息产业浪潮。物联网通过传感设备获取“物”信息,并通过网络实现信息交换,以实现智能化识别、定位、跟踪监控和管理的目的。基于物联网的车间生产过程异常状态监控系统越来越多,这类系统通过采集生产车间的数据并进行分析处理,以实现车间智能化管理从而提高企业的经济利益。但在生产车间监控系统中,参与信息交互的对象包含人、机、物等不同类型对象,系统需要处理的是大量结构异质的信息,同时随着车间规模的扩大,监控也变得更加复杂,无法保证监控系统投入运行之前完全符合设计要求。因此,提出一种车间生产监控系统建模和验证方法,在系统实施之前使用形式化方法对生产车间监控系统建模并验证,尽早发现系统设计的不合理和不正确之处,显得尤为必要。本文以物联网环境下离散生产车间异常监测系统为研究背景,研究了基于时间自动机的时序约束活动异常监测系统形式化验证方法,利用时间自动机验证方面的优势验证监测系统设计的有效性和完备性。本文首先综述了复杂事件检测的国内外研究现状;分析了生产车间现场的若干特征,定义了基于时间自动机的生产车间现场模型,用状态不变式中的时间约束刻画操作人员等的自主随机性,用状态和变迁分别刻画不同类型的活动,同时对生产对象的感知行为抽象表示;然后说明了不同的事件使用策略和消耗策略建模方法,分析了事件和事件约束模型构造方法,并提出了复合事件模式采用若干时序相关事件操作符的时间自动机模型构造方法,其中提出了控制模型时间自动机建模方法,控制模型减小了一个事件模式对应自动机模型的规模;接着为了简化异常监测时间自动机模型性质验证,建立了包含正常生产情况的辅助生产过程自动机模型;针对生产车间异常监控系统的特点,提出从系统功能性、实时性、冗余性及未定义的异常行为四个方面验证系统设计的正确性和完备性;最后使用时间自动机验证工具UPPAAL,以粘合加工车间异常监测为例,对提出的方法进行了验证。本文的研究表明:时间自动机形式化方法能够较好刻画生产车间异常监测系统的相关特性。利用时间自动机形式化建模及验证方法,能够有效发现监测系统潜在的问题,并在一定程度上辅助监测系统的开发设计,并为相关人员提供有效改进依据。实验结果证明本文提出的方法有一定应用价值和参考意义。(本文来源于《大连理工大学》期刊2017-06-11）
陈志辉,吴敏敏[5]（2015）在《时间约束条件下Web服务组合的形式化分析与验证》一文中研究指出随着Web技术和商业应用的快速发展,Web服务组合技术已成构建电子商务应用的主要方法之一。当前,为适应快速变化的商业环境,对商业应用提出了实时性的要求,即限定服务的行为必须满足给定的时间约束条件。文中提出了一种形式化方法,用于分析与验证Web服务组合的时间约束行为。首先,扩展了Web服务接口描述语言,增加对时间约束的描述,然后定义一种时间行为自动机,用于刻画Web服务组合的时间行为,最终利用模型验证技术来自动验证这些行为是否满足给定的时间属性。通过对股票分析应用场景以及使用UPPAAL模型验证工具,表明该方法的可行性和有效性。(本文来源于《贵州大学学报(自然科学版)》期刊2015年05期）
陈志辉[6]（2015）在《时间约束条件下web服务组合的形式化分析与验证》一文中研究指出随着Web技术和商业应用的快速发展,面向服务的计算(SOC)和面向服务的体系结构(SOA)也已成为人们关注的焦点。由于两者的出现,有效解决在分布以及异构环境下软件集成与复用。当前,日益成熟的Web服务技术也为两者提供了有效地技术支撑。Web服务是一种基于网络的具有松耦合、独立性强等特点的软件构件。服务是Web体系中交互的基本单位。由于单个Web服务的功能有限,web服务组合技术已成构建电子商务应用的主要方法之一。然而,如何确保在复杂环境下的Web服务能够保证软件的质量,满足人们的预期呢?特别是限定服务的行为必须满足给定的时间约束条件。形式化技术作为软件质量保证的一种重要方法。当前,为适应快速变化的商业环境,对商业应用提出了实时性的要求。即文中提出了一种形式化方法,用于分析与验证web服务组合的时间约束行为。首先,扩展了Web服务接口描述语言,增加对时间约束的描述,然后定义一种时间行为自动机,用于刻画web服务组合的时间行为,最终利用模型验证技术来自动验证这些行为是否满足给定的时间属性。通过对股票分析应用场景以及使用UPPAAL模型验证工具,表明该方法的可行性和有效性。深入研究服务组合建模与验证技术可以保障服务组合的可靠性。(本文来源于《华侨大学》期刊2015-05-30）
鱼先锋,王辉[7]（2011）在《并发系统互斥约束的形式化验证》一文中研究指出并发系统的模型是其性能评价、仿真、作业调度及控制的研究基础。互斥是并发系统最重要的性质之一,建立了具有互斥约束系统的一般数学模型———互斥模型。将模型互斥性分解为安全性、活性和无阻性约束,形式化规约成LTL公式;给出了基于不动点的互斥模型的模型检测算法。并结合实例进行了互斥模型的形式化验证,给出了模型精化改进的详细过程。随着并发系统进程增加,不动点模型检测算法会面临状态爆炸问题,给出了另一种基于布尔公式的BDD(二叉决策树)运算下的符号化模型检测方法,有效地缓解了状态爆炸问题。(本文来源于《商洛学院学报》期刊2011年06期）
谭力[8]（2010）在《基于情态演算的UML形式化验证与OCL约束自动生成研究》一文中研究指出从软件工程中软件生命周期的角度分析,软件架构是软件的核心结构与行为,因而软件架构的设计是软件设计的核心,也是随后进行代码开发的基础。因此软件架构设计的重要性不言而喻。由于软件架构设计本身是一种建模活动,如何对软件架构设计的标准建模语言UML进行正确性验证是一个难题。传统软件验证方法有着不够精确、非自动化等不足。另外,对UML进行正确性验证需要得到UML的形式化语义,而UML本身是一种图形化的表示方法,不具有形式化的语义。因此本文将采用形式化方法来对UML模型进行形式化描述,即为其赋予等价的形式化语义,再根据其语义进行形式化验证。为了进一步精确描述UML模型的语义,为其提供OCL约束是一种主流方法。而OCL约束需要人手工编写,同样具有正确性难以保证、人员开销等问题,因此为UML模型自动生成OCL约束模板是一种很好的解决方法,生成的OCL模板可供软件设计人员参考,从而提高了软件工程的整体效率。本文也将对OCL约束自动生成进行研究。UML是软件设计过程事实上的标准建模语言。本文首先从历史发展、子图种类、建模工具和以XMI表示的UML四个角度对UML作了简要的介绍,并具体介绍了即将研究的两种UML子图：类图和状态图。同时介绍了形式化方法的基本概念和主要分支，并总结了国内外现有的对UML形式化的研究。最后介绍了UML的标准子语言OCL、采用的形式化语言情态演算和它的具体实现——逻辑编程语言Prolog,并进一步分析了从UML转换到情态演算的可行性,从理论上确定了给出的解决方案的正确性。本文随后给出了基于情态演算的UML形式化描述方法。首先分析了选择UML类图和状态图作为研究对象的意义,再分别对UML类图和状态图进行形式化描述：先是给出了两种子图的一种形式化语义结构；再分析了两种子图元素与数理逻辑和情态演算元素的对应关系；又提出了两种子图到数理逻辑语句和Prolog代码的转换算法,并以伪代码的形式给出。然后着重定义了UML模型的两种基本错误类型：领域无关的UML模型语法错误和领域相关的UML模型语义错误,并给出具体错误实例和自动生成的Prolog代码。进一步,本文讨论了如何实现对UML模型的OCL约束模板自动生成。首先强调了OCL约束自动生成的研究意义,同时给出了OCL约束的应用范围。从而进一步分析了如何在UML模型中提取OCL约束的目标应用对象,并给出了一种提取算法。最后给出了该提取算法的Perl示例代码的具体实现。作为上述理论的补充和可行性证明,后续章节详细介绍了以UML子图到情态演算的转换算法和OCL约束模板自动生成算法为基础而设计并实现的UML形式化验证原型工具USCVSC。首先建立了该原型工具的系统实现框架和代码框架。其次给出了该原型工具的用户界面,并详细描述了其中的4个基本子功能界面。最后说明了,通过此原型工具,可以实现UML模型语法检查和语义错误验证,以及OCL约束模板自动生成的综合性功能。最后,本文对USCVSC原型工具的使用进行了介绍,并结合一个大学教学系统和大学申请系统的实际案例来对原型工具的基本功能进行演示。先描述了该应用实例的特点,并用UML建模工具对其类图和状态图进行设计。接下来则利用USCVSC原型工具对预定义的UML模型错误进行验证：对于UML语法错误的检查可以在USCVSC原型工具中完成,对于UML语义错误的验证则需要USCVSC原型工具和Prolog解析器一起协同完成。最后演示了如何利用USCVSC原型工具为UML类图自动生成OCL约束模板,并给出了示例OCL约束语句。综上所述,本文以形式化语言情态演算为描述语言来对UML模型进行形式化验证以及自动生成OCL约束,并最终实现了原型工具。使得UML模型中多初始状态、监护条件中无逻辑运算符等语法错误得以发现,同时也能验证出UML模型中需求不完整和需求逻辑错误等语义错误。从而能帮助软件设计人员修正最初的UML模型设计,避免在软件工程后续阶段不必要的系统开销。最终达到使软件工程各阶段的整体效率得到提升的目标,为软件工程自动化做出了贡献。(本文来源于《华东师范大学》期刊2010-04-01）
齐玉华,郭天杰,陶政德,程春华[9]（2009）在《形式化可测性约束在软件模型实现过程中的研究》一文中研究指出在软件测试中,软件使用模型反映实际运行场景的能力是直接决定测试的成功与否的关键因素之一。一般可以通过对在需求分析阶段已生成的UML建模进行研究得到使用模型,但原始的UML模型,由于缺乏严格的定义及必要的约束,如果要生成高精度的软件模型,必须对其添加必要的形式化可测性约束。这正是文章研究的重点。(本文来源于《舰船电子工程》期刊2009年09期）
宋英杰[10]（2009）在《基于OCL的Web服务组合形式化约束研究》一文中研究指出当前流行的Web服务和Web服务组合真正进入实用阶段还面临着诸多问题。目前,语法层次和语义层次的组合方法仍处于初级阶段,这两种方法都缺乏严格的形式化语义支持,容易出错且不容易检测;这两种方法的组合语言均以WSDL标准为基础,侧重于服务间的消息传递,缺乏对Web服务行为的有效约束,容易导致组合后系统行为与设计阶段的系统行为相偏离,还可能导致系统动态演化过程中的行为不一致。对象约束语言OCL作为UML标准的一部分,是可以用来描写清晰、明确风格的表达式的标准语言。本论文将OCL引入到Web服务组合过程中,为Web服务组合增加语义信息。本论文首先对目前国内外的研究现状和研究成果进行了分析,在简要介绍Web服务、Web服务组合及OCL的相关理论和相关技术之后,深入研究Web服务组合中可能存在的不匹配和异常情况,将OCL的形式化描述方法应用到Web服务组合中,针对服务间的端口类型、端口个数、分支结构、互斥和互补等情况进行约束,对服务组合进行约束检测以减少这些不匹配和异常情况的发生。根据对象约束语言在Web服务中的形式化描述,设计和实现了对象约束语言在Web服务组合语言可视化编辑器中翻译执行。对Web服务组合增加的形式化约束有利于提前发现Web服务组合中可能存在的异常情况,是提高Web服务组合执行的成功率和增强用户满意度的关键,对服务组合的正确运行具有十分重要的意义。(本文来源于《大连海事大学》期刊2009-05-01）
形式化约束论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
随着实时嵌入式系统在汽车和航空电子等领域的复杂性和安全性日益突出,应用严格分析技术以确保系统可预测就显得非常重要。因此统一建模语言UML采用了 MARTE(Modeling and Analysis of Real-Time and Embedded Systems)作为其在实时嵌入式系统领域的扩展,提供了规范、设计和验证平台的支持。MARTE提供了一个丰富的时间模型,当使用MARTE时间模型时,许多相互依赖的时钟要在模型中定义,而这种时钟的相互依赖关系可以由一门专用的语言指定,称之为时钟约束语言(CCSL)。CCSL指定了时钟间同步和异步的约束关系,为MARTE模型上的因果时序分析提供了支持。一个重要的问题是验证描述系统模型时间需求的CCSL约束的可满足性,这个问题能够帮助开发人员在系统设计阶段发现缺陷,从而避免在开发阶段带来不必要的损失。目前许多研究人员都在探寻CCSL的形式化分析方法,主要是利用迁移系统、Promela语言、Buchi自动机、时间自动机、重写逻辑等对CCSL约束进行转换,结合相应的工具进行分析验证。然而有些方法需要不寻常的中间转换过程,容易导致出错或者效率低下。有些转换方法不能转换所有的约束或者只考虑了部分约束的转换。基于状态的转换方法容易导致状态爆炸,影响分析效率。本文提出基于SMT的统一而高效的CCSL形式化分析方法,可用于CCSL的可调度分析、LTL模型检测、死锁检测、蕴含关系证明以及迹分析,依托于高效的SMT求解器Z3和CVC4进行分析和验证。将CCSL约束转换成SMT公式的过程是十分自然的,避免了复杂的中间转换过程,从而降低了出错的风险。不同于一些方法只能转换部分CCSL约束,CCSL约束到SMT公式的转换没有这个限制。众所周知,基于SMT的方法能够有效的克服模型检测的状态爆炸问题,利用该方法提升了对CCSL约束进行模型检测的效率。同时基于SMT的方法还能通过理论证明来证明CCSL约束具有一些属性,这是大部分现有的对于CCSL形式化分析方法缺少的。本文不仅交代了基于SMT的CCSL形式化分析方法在五个方面上的理论实现,而且给予相应的实际例子表明方法的可行性和有效性。自主开发了一个CCSL的分析验证工具,集成提出的方法,并应用了一个铁路联锁系统的案例。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
形式化约束论文参考文献
[1].付春艳.基于Event-B的adhoc路由协议及任务级时间约束的形式化建模与验证[D].浙江大学.2019
[2].应云辉.基于SMT的时钟约束语言CCSL形式化分析与应用[D].华东师范大学.2018
[3].应云辉,张民.基于SMT的时钟约束语言CCSL的形式化分析方法与工具[J].软件学报.2018
[4].查欣欣.基于时间自动机的时序约束活动异常监测系统形式化验证[D].大连理工大学.2017
[5].陈志辉,吴敏敏.时间约束条件下Web服务组合的形式化分析与验证[J].贵州大学学报(自然科学版).2015
[6].陈志辉.时间约束条件下web服务组合的形式化分析与验证[D].华侨大学.2015
[7].鱼先锋,王辉.并发系统互斥约束的形式化验证[J].商洛学院学报.2011
[8].谭力.基于情态演算的UML形式化验证与OCL约束自动生成研究[D].华东师范大学.2010
[9].齐玉华,郭天杰,陶政德,程春华.形式化可测性约束在软件模型实现过程中的研究[J].舰船电子工程.2009
[10].宋英杰.基于OCL的Web服务组合形式化约束研究[D].大连海事大学.2009