导读:本文包含了形式化系统论文开题报告文献综述及选题提纲参考文献，主要关键词:形式化方法,智能系统,组合抽象模型,模型检测
形式化系统论文文献综述
周益龙,韩斌[1]（2019）在《基于层次组合抽象的智能系统形式化验证》一文中研究指出论文针对智能系统提出了一种形式化建模和验证的方法:首先,采用层次化的思想将智能系统分为应用层、系统层和设备层,综合系统功能需求和硬件模块分别建立各层的Kripke结构模型;然后,根据组合模型规则将层次模型进行组合,经过抽象处理后得到系统组合抽象模型。最后,以能源共享系统为例,用CSP#描述系统模型、LTL描述系统性质,利用PAT工具完成系统模型的自动验证。实验结果表明,该方法综合考虑了系统各个主体的行为,能够有效找出智能系统中的设计缺陷,并且可以缓解模型检测中的状态空间爆炸问题。(本文来源于《计算机与数字工程》期刊2019年08期）
胡军,张维珺,李宛倩[2]（2019）在《面向需求的安全关键系统形式化建模与验证方法研究》一文中研究指出在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML~(-e)语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML~(-e)模型转化成NuSMV 2模型的方法,并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。(本文来源于《计算机工程与科学》期刊2019年08期）
张丹涛,田贝,张馨洋,朱立平[3]（2019）在《基于形式化方法进行复杂逻辑系统的验证》一文中研究指出近年来,民用航空系统复杂度越来越高,随之而来的是其安全性和可靠性等非功能性需求越来越庞大,造成的结果是难以通过传统的测试方法完成软件功能的全覆盖测试,特别是在复杂逻辑控制领域,如自动驾驶仪、控显等,其状态空间往往超过了1010～1020的规模。在理论层面,对于大规模状态空间,一般采用形式化方法进行数学推演完成穷举测试,但是早期的系统需求和设计往往基于自然语言描述,不具备形式化验证的基础。近年来,随着基于模型的方法在系统和软件领域的推广使用,使得系统或软件逐步具备了半形式化或形式化的描述方式,形式化验证技术也开始随之得到了更广泛的应用。本文以飞行控制模态管理项目为基础,介绍了几个主流形式化验证方法的工程应用及验证结果,说明了该方法在高可靠高安全民用飞行控制领域应用的可行性和实用性。(本文来源于《2019年（第四届）中国航空科学技术大会论文集》期刊2019-08-15）
邹佳霖,范宝德,韩兆玉[4]（2019）在《基于Petri网的MES系统形式化建模》一文中研究指出针对一般车间执行制造系统结构复杂性高、重构能力弱、性能分析困难等问题,以水产品加工MES系统为例,通过Petri网对其进行形式化分析与建模.对水产加工的流程进行逐级分解、细化,根据功能将整个系统划分成3个模块,基于Petri网分别对3个模块进行集成建模.最后根据Petri网理论知识,对MES的Petri网模型复杂度与结点特性进行分析和研究,建立一种行业通用的、结构简单易扩展、灵活性强的Petri网模型.(本文来源于《烟台大学学报(自然科学与工程版)》期刊2019年03期）
屈胤达[5]（2019）在《高速磁浮列控系统运行场景构建与形式化验证》一文中研究指出高速磁浮技术作为区别于轮轨高铁的新型交通运输手段,是未来高速和特高速轨道交通系统发展的重要方向。近年来,我国对高速磁浮列车技术开展了相关研究,计划在未来五年之内建成时速600公里条件下的高速磁浮试验线。高速磁浮列车运行控制系统作为保证列车安全运行的关键,其工程应用方面的研究已刻不容缓。高速磁浮列控系统的工程应用需要相应的场景规范来进行指导,由于运行机理的区别,成熟的轮轨高铁列控系统运行场景无法照搬在高速磁浮列控系统上,而目前国内也没有系统的开展过高速磁浮列控系统运行场景方面的研究。本文从高速磁浮试验线列控系统的研发和建设出发,对高速磁浮列控系统的运行场景进行了相关研究,主要工作如下:首先,提出了统一建模语言UML结合通信顺序进程CSP的高速磁浮列控系统运行场景分析方法,制定了 UML模型和CSP模型之间的转换规则,给出了方法的具体内容和流程;其次,根据高速磁浮列控系统的系统结构和功能特点,构建了 9个高速磁浮列控系统的运行场景,并对每个运行场景的场景术语、交互信息和交互流程进行了规范化的描述;然后,对构建的场景进行了建模与形式化验证。按照提出的高速磁浮列控系统运行场景分析方法,分别建立了启动与登录、停车点步进和分区切换场景的UML模型和CSP模型,利用ProB工具验证了场景的逻辑正确性;最后,基于运行场景对高速磁浮试验线列控线路数据进行了工程设计,利用MATLAB中的Simulink组件建立了列车正常运行场景下的仿真模型,对初版的列控线路数据进行了仿真分析,修正了其中不合理的设计。图81幅,表17个,参考文献72篇。(本文来源于《北京交通大学》期刊2019-06-03）
张卫祥,刘文红,魏波[6]（2019）在《基于形式化模型的航天测控软件系统测试》一文中研究指出软件系统测试是一种重要的测试类别.作为大规模安全攸关系统,航天测控软件系统软件数量多、信息交换关系复杂、安全可靠性要求高,对航天测控软件系统开展软件系统测试是工程实践中的一个难题.结合工程实例,提出了一种基于形式化模型的软件系统测试方法.首先对软件功能、性能、接口等进行抽象,给出软件系统的形式化定义;其次提出线索分析的不同策略,识别软件系统测试需求;然后开展软件系统的流程、阶段和场景分析,建立可刻画软件系统级行为的场景树模型;最后提出基于场景树模型的测试覆盖准则,给出形式化静态检查和动态测试用例生成方法,生成测试用例集合.实例验证表明方法是有效的和可行的.(本文来源于《第31届中国控制与决策会议论文集（3）》期刊2019-06-03）
张锦坤,杨孟飞,乔磊,杨桦,刘波[7]（2019）在《基于有限状态机的操作系统需求层形式化验证》一文中研究指出操作系统是航天器必备的基本软件,操作系统的可靠性和安全性直接关系航天型号任务的成败.虽然目前已采用多种手段对操作系统进行可靠性和安全性保障,但仍存在不能完全排除缺陷的情况,因此对空间操作系统开展形式化验证研究势在必行.需求层验证是操作系统形式化验证的一部分,本文在分析操作系统需求的基础上,采用有限状态机在操作系统需求层进行形式化描述,并针对应用在某航天器上的SpaceOS2在需求层进行了建模,相应地在定理证明工具Coq中进行了描述建模;然后定义了六条操作系统应满足的全局性质并进行了形式化描述,给出了系统模型满足这些性质的机器可检查的证明.证明结果表明采用有限状态机方法对操作系统需求层进行形式化验证是可行的,为进一步全面形式化验证奠定了基础.(本文来源于《空间控制技术与应用》期刊2019年02期）
王陈[8]（2019）在《基于Event-B形式化方法的免疫系统模型研究》一文中研究指出在当今社会中,社会信息化高速发展,每一个行业都与软件紧密相关。在开发一个软件时,首先要做的是对软件需求进行分析,而在这个分析描述的过程中又避免不了因语法或语义带来的错误。为了减轻这些不必要的错误带来的损失,形式化方法应运而生。目前形式化方法领域中,比较常见的两种方法是B方法和Event-B方法,Event-B方法由B方法演化而来,具有许多B方法没有的优点,并且Event-B方法在工具平台上有着很大的优势。Rodin平台是基于Eclipse开发的集成环境,为Event-B方法提供了系统级的开发模式,可以通过逐层精化的方式为模型添加所需的属性和功能,并且Rodin平台简化了 Event-B方法的验证过程,提供了多种自动证明器,支持更多的证明义务,为模型的精化和证明提供了有效的支持,同时最小化对更改现有证明的影响,在软件开发的前期就保证了软件模型的正确性和一致性。本文以免疫系统作为开发需求,使用Event-B方法建立免疫系统抽象模型,并详细阐述在Rodin平台下对该模型从需求分析到验证的全部过程,主要开展了如下工作:(1)研究了现阶段常用的形式化方法B方法与Event-B方法各自的建模方式,介绍了 B方法的开发过程和优缺点,并在此基础之上针对免疫系统的需求对两种方法作出比较,特别是精化方式和交互式证明方面,阐述选择Event-B方法进行免疫系统建模的原因。(2)研究以免疫系统为例的Event-B形式化方法的建模过程,创建免疫系统初代抽象模型,然后通过逐步精化的方式向模型中添加属性和功能,使系统更加完善,直至满足所有的需求。(3)研究在Rodin平台上的抽象模型验证方式,介绍了几类自动证明器和免疫系统抽象模型证明中所使用到的证明义务,并联系免疫模型进行了推理演示。最后,通过交互式证明的方式完成整个免疫模型的证明。总的来说,Event-B形式化方法能够很好的帮助开发人员完成对软件系统需求准确性和一致性的验证。本文通过建立基于Event-B方法的免疫系统抽象模型,详细地展示了从需求重写到模型验证的全过程,体现了在软件开发前期使用形式化进行模型验证的重要性。(本文来源于《扬州大学》期刊2019-04-01）
解云月[9]（2019）在《Spark系统的形式化建模与性能分析》一文中研究指出Spark作为一个分布式大规模数据计算处理框架,由于其优异的性能表现和兼容性,它的用户数量一直在大量增长,而通过对它进行性能评价可以最大化地利用系统资源,减少系统空闲率。性能评估进程代数(Performance Evaluation Process Algebra,PEPA)是随机进程代数的一种,它用代数的方式构建系统模型,将系统分解成几个交互的组件,能够比较清晰地反映系统的层次结构,降低模型构建和分析的难度。随机Petri网(Stochastic Petri Nets,SPN)既有直观的图形描述,也有严格的公式定义,能够较为清晰地反映系统状态的变化过程。本文针对Spark系统的性能评价与分析展开研究,主要研究内容包括以下叁个方面:一、构建Spark系统的形式化模型。通过分析Spark系统的整体架构和运行流程,将Spark系统抽象为多个交互的组件,从而得到系统的PEPA模型。根据转换规则将PEPA模型转换成SPN模型,并分别给出两个模型的相关参数。二、提取Spark系统模型的性能指标。分别对得到的两种模型采用流逼近方法和随机模拟方法来提取模型中重要的性能指标:响应时间、利用率和吞吐量。为了模拟系统中执行某个服务的过程,本文提出了服务流获取算法和响应时间模拟算法。通过追踪变迁的转移获得执行某条服务流的时间,最终得到系统在稳态情形下的响应时间。针对PEPA模型,则采用了一种近似求解的流逼近方法,该方法通过微分方程组来逼近系统状态的转移过程。叁、评价并分析Spark系统的性能。从响应时间、利用率和吞吐量叁个维度对Spark系统的性能进行了评价与分析。通过分析系统的各项参数对系统性能指标的影响来完成Spark系统的性能评价。(本文来源于《扬州大学》期刊2019-04-01）
汪一飞[10]（2019）在《Laplace变换在Coq中的形式化及其在飞控系统验证中的应用》一文中研究指出形式化数学是一个借助定理证明器进行数学定理机械验证的研究方向。形式化工程数学是形式化数学技术在工程数学领域中的应用。在控制系统设计中的一个关键性数学工具是Laplace变换,它被广泛地应用于求解线性微分方程和分析安全关键系统,它也是包括飞行控制系统在内的许多控制算法设计和软件设计的基础工具。定理证明是利用计算机辅助人们进行数学定理证明,它克服了纯人工证明容易出错等缺点,已经广泛应用于数学定理证明、集成电路和软件验证中,然而在飞行控制方面的形式化验证工作十分罕见。一个典型的例子是采用SCADE系统进行建模、开发和验证飞行控制软件,虽然基于模型的方法提高了软件生产力并且减少了软件缺陷,但是并不能解决数学推导和飞控数学算法的可靠性验证问题。飞行控制系统的设计和分析依赖于大量复杂的数学推导,为了解决这样的问题,我们研究基于Coq定理证明器的形式化工程数学验证技术。这一工作的大方向是在Coq中建立完善的形式化工程数学理论库,以便支持飞行控制数学以及其他工程数学的推导验证。本文在高阶逻辑定理证明器Coq中采用极限、连续、微分、积分、复数等理论实现了Laplace变换定义的形式化,并且验证了Laplace变换的主要性质:存在性、线性性质、复频域位移性质、微分性质、二阶微分性质、积分性质等。为了能验证更复杂的控制系统,本文给出了二维向量Laplace变换的形式化定义,并且验证了向量Laplace变换基本性质。目前尚未在文献中发现将Laplace变换形式化理论推广到二维向量的类似工作,这一工作已经能够有效支持实际应用中大部分控制系统的形式化验证。二维Laplace变换依赖于矩阵理论,我们采用基于元组的表示方法对小规模的矩阵(2-4维)进行形式化定义并且对矩阵的运算、向量的运算以及矩阵和向量之间的运算进行形式化定义。在此基础上,我们对这些矩阵运算的正确性以及运算性质进行形式化证明。最后我们对飞行控制系统、机器人控制系统中的一些传递函数的推导过程进行了形式化的描述和验证。(本文来源于《南京航空航天大学》期刊2019-03-01）
形式化系统论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
在安全关键系统领域中,明确的需求对于一个系统的作用至关重要。使用基于模型的系统工程思想对自动飞行控制系统进行面向需求的形式化建模与验证,使用RSML~(-e)语言对自动飞行控制系统(AFCS)需求进行建模,提出一种将RSML~(-e)模型转化成NuSMV 2模型的方法,并用NuSMV 2对模型的属性进行验证。针对一个真实综合航电系统中的自动飞行控制系统GFC700进行分析验证,实验结果表明,该方法对实际系统的安全性分析具有可行性。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
形式化系统论文参考文献
[1].周益龙,韩斌.基于层次组合抽象的智能系统形式化验证[J].计算机与数字工程.2019
[2].胡军,张维珺,李宛倩.面向需求的安全关键系统形式化建模与验证方法研究[J].计算机工程与科学.2019
[3].张丹涛,田贝,张馨洋,朱立平.基于形式化方法进行复杂逻辑系统的验证[C].2019年（第四届）中国航空科学技术大会论文集.2019
[4].邹佳霖,范宝德,韩兆玉.基于Petri网的MES系统形式化建模[J].烟台大学学报(自然科学与工程版).2019
[5].屈胤达.高速磁浮列控系统运行场景构建与形式化验证[D].北京交通大学.2019
[6].张卫祥,刘文红,魏波.基于形式化模型的航天测控软件系统测试[C].第31届中国控制与决策会议论文集（3）.2019
[7].张锦坤,杨孟飞,乔磊,杨桦,刘波.基于有限状态机的操作系统需求层形式化验证[J].空间控制技术与应用.2019
[8].王陈.基于Event-B形式化方法的免疫系统模型研究[D].扬州大学.2019
[9].解云月.Spark系统的形式化建模与性能分析[D].扬州大学.2019
[10].汪一飞.Laplace变换在Coq中的形式化及其在飞控系统验证中的应用[D].南京航空航天大学.2019