导读:本文包含了非形式化方法论文开题报告文献综述及选题提纲参考文献，主要关键词:内控信息化技术,研究方法,形式化的具体方法
非形式化方法论文文献综述
师新峰[1]（2019）在《企业内控信息化实施的规范化方法研究——基于领域分析与形式化方法》一文中研究指出伴随着现在经济发展得越来越快,一些企业内部开始实施信息技术手段来进行内控管理,其中包括制定一些规范制定和企业流程具体的措施方案,以此来完成我们将信息化系统提高到企业内部需求的信息化管理平台的高度。早在二零零二年以后开始,美国自从颁布了萨班斯法案以后,各个国家开始对内部控制的认识达到了一个非常高的高度,与此同时我们国家在二零一零年开始,先后颁布了相关类型的文件,以此标志着在我国企业内部信息化体系正式完成。由于我们掌握度理论多于实践,这其中很多的地方还存在着一定的问题需要我们解决。(本文来源于《大众投资指南》期刊2019年16期）
张丹涛,田贝,张馨洋,朱立平[2]（2019）在《基于形式化方法进行复杂逻辑系统的验证》一文中研究指出近年来,民用航空系统复杂度越来越高,随之而来的是其安全性和可靠性等非功能性需求越来越庞大,造成的结果是难以通过传统的测试方法完成软件功能的全覆盖测试,特别是在复杂逻辑控制领域,如自动驾驶仪、控显等,其状态空间往往超过了1010～1020的规模。在理论层面,对于大规模状态空间,一般采用形式化方法进行数学推演完成穷举测试,但是早期的系统需求和设计往往基于自然语言描述,不具备形式化验证的基础。近年来,随着基于模型的方法在系统和软件领域的推广使用,使得系统或软件逐步具备了半形式化或形式化的描述方式,形式化验证技术也开始随之得到了更广泛的应用。本文以飞行控制模态管理项目为基础,介绍了几个主流形式化验证方法的工程应用及验证结果,说明了该方法在高可靠高安全民用飞行控制领域应用的可行性和实用性。(本文来源于《2019年（第四届）中国航空科学技术大会论文集》期刊2019-08-15）
马振威,陈钢[3]（2019）在《基于Coq记录的矩阵形式化方法》一文中研究指出矩阵在工程系统中有广泛的应用,矩阵运算的正确性对工程系统的可靠性有重要影响。Coq是一种基于带类型λ演算的功能强大的高阶定理证明器。虽然Coq类型系统能够很好地描述可变大小的动态数据类型,但是对于固定大小的类似向量和矩阵的数据类型,其缺乏满意的描述机制。Coq库中也没有向量库或矩阵库,因此在使用Coq来对涉及矩阵的定理或算法进行形式化验证时十分复杂。针对这些问题,文中提出了一种基于Record类型的矩阵实现方法并定义了一组基本的矩阵函数,证明了它们的基本性质。基于文中提供的矩阵类型和相关引理可以比较轻松地完成飞行控制转换矩阵的验证。同其他矩阵实现方法相比,所提方法不仅在实现上相对简洁,在使用上也更加简单、方便。(本文来源于《计算机科学》期刊2019年07期）
王陈[4]（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）
陈金凤[5]（2019）在《形式化方法在自动代码生成中的研究与应用》一文中研究指出自改革开放以来,计算机领域也进入飞速发展的阶段,给人们带来了极大的变化。未来,以计算机为基础的各类研究及开发应用将加快推动社会的发展。自动代码工具的产生,能够在很大程度上解放人们的双手,使得软件开发的效率得到进一步提高。但是随着开发系统的规模和复杂度的不断增加的同时,软件开发的错误率也随之增加。如何在软件开发初期,提高需求描述的准确性和代码的一致性,变得尤为重要,现已成为目前软件工程研究领域的一个热点。统一建模语言UML是面向对象技术中使用最为广泛的一种可视化建模语言。它定义良好、易于构建和文档化~([1])。但是半结构化的UML模型缺乏形式化语义,难以使用数学方法对其进行分析和验证,对模型的完整性和正确性的验证也难以判定。因此,在自动代码生成过程中,对UML模型进行精确语义和分析的形式化描述显得尤为重要。形式化方法产生于20世纪50年代,是一种基于严格数学基础的技术,对提高软件系统的正确性有非常显着的作用,是当今软件开发中最为严谨的方法。本文在统一建模语言UML和形式化方法理论的基础上,将形式化方法加入到自动代码生成过程中,使得UML模型的语义表达的更精确,生成的代码更具有代表性。本文通过研究对UML模型图的形式化方法转换的理论和示例学习,完善UML模型到形式化方法的转换规则,并制定形式化方法与面向对象语言Java代码之间的转换规则。本文主要做了以下几方面的工作:(1)首先对UML和B形式化方法的理论进行分析研究,由于自然语言描述下的UML语义不够精确。而B形式化方法可对软件系统提供无二义的、更精确的描述。两者的结合对提高软件的可靠性具有积极作用。(2)在对UML状态图模型和B抽象机符号进行详细分析的基础上,学习现有对UML模型的形式化转换的理论。再通过UML模型与B形式化方法之间存在的映射关系,完善从UML状态图到B抽象机的转换规则。(3)在代码生成阶段,制定B形式化方法与面向对象语言Java两者之间的映射规则。(4)完成对自动代码生成的程序编写,使用Java语言在Eclipse开发平台上实现模型转换的实现工具。并通过案例来验证本文提出的方法是有效可行的。(本文来源于《华北电力大学》期刊2019-03-01）
张维珺[6]（2019）在《基于形式化方法的系统需求建模与安全性分析研究》一文中研究指出随着计算机的诞生及快速发展,其在各行业、各领域得到广泛应用,在安全关键系统中起着举足轻重的作用。对于安全关键系统而言,计算机的偶发故障或系统失效常常会带来危及生命、财产的重大损失。因此对安全关键系统,如飞机机载系统的安全性分析至关重要,不仅需要保证系统的正常功能行为是否完备,还需要在系统的需求分析及模型设计过程中充分的考虑可能的系统功能失效影响和处理故障的方式。形式化方法是一类基于逻辑形式语言的数学建模与分析方法,能够用于安全关键系统的建模、分析与验证,提高安全关键系统的安全性。针对航空安全关键系统需求的安全性,本文展开了一种基于形式化方法的系统需求建模与分析研究,具体包括以下几个方面:(1)设计了一个基于四变量模型的面向需求的建模与安全性分析框架。在这个框架中根据安全关键系统的需求规约的重要性,基于四变量模型思想对系统进行分析,采用基于四变量模型的形式化表格语言SCR对系统进行需求建模,验证SCR模型的需求完整性,并将整套思想运用在飞行引导系统的建模与需求完整性分析中;根据系统需求规约、模型转换和模型检验的思想,提出了一套基于NuSMV模型检验的需求验证框架;能够基于MBSA思想,对系统进行故障行为设计以及故障分析等。(2)提出了一套将SCR模型转换为NuSMV模型的转换方法。由于基于四变量模型的SCR模型仅能验证系统需求的完备性,不能够检验系统功能性属性,因此需要将其转换为可以进行功能性属性验证的NuSMV模型。本文研究了SCR语言与NuSMV语言的语法语义及其特征,提出了两种语言间的模型转换方法,能够保证语义一致性,包括类型与变量的转换、时态间的对应以及SCR语言中模式及项到NuSMV语言中子模块的转换等。(3)建立了基于故障注入机制及模型扩展思想的系统验证与安全性分析过程。该过程包括根据系统行为特征设计系统故障行为,对系统正常行为模型进行故障注入,识别系统顶事件,对系统正常行为模型进行模型扩展得到故障扩展模型以及进行故障分析等。(4)针对一个真实的综合航电系统进行了需求建模及安全性的实例分析。包括分析飞行引导系统的架构特征,特别是其所包含的模式逻辑;基于四变量模型思想对该实例系统进行了需求分析,使用SCR语言对其进行需求建模,并进行需求完整性分析;将SCR模型转换为NuSMV模型,验证系统功能性属性的正确性;构造多种故障模式对实例系统进行故障分析,生成故障树和FMEA表等。(本文来源于《南京航空航天大学》期刊2019-03-01）
黄健[7]（2019）在《携手形式化方法 守望计算之春——记上海交通大学电子信息与电气工程学院特别副研究员符鸿飞》一文中研究指出伴随着区块链概念的大火,整个金融市场似乎都显得异常兴奋,可在区块链概念被越来越多的人所知晓的同时,金融市场的不景气也在迫使区块链的浪潮逐渐退去。但不可否认的是,在这个过程中,区块链领域也取得了一些实质性的进步。其中,形式化验证的应用就是极为重要的一方面。如果说在几年前,形式化验证还处于理论研究阶段,如今,几年后的形式化验证已经摇身一变,相继在工业(本文来源于《中国科技奖励》期刊2019年02期）
王恪铭,王峥[8]（2019）在《基于形式化方法的道口控制系统规范建模与验证》一文中研究指出为了增强铁路道口控制系统设计的可靠性,使用一种形式化方法对该系统进行建模与验证.基于道口管理规范,在分析系统各类属性与事件流程的基础上,使用UML图方法并结合精化策略建立了系统各层的Event-B语言模型.通过对不变式的证明义务进行证明,验证了系统设计中的安全、时间特性,检查出了需求规范分析中的缺陷,提出了增强系统稳健性的改进方案,修正了系统的设计原型.最后,通过不变式冲突与死锁检验进一步确认了模型的正确性.研究表明文中方法提高了形式化建模过程的准确性与层次性,且确认得出目前规范中存在列车驶入道口时不能确保道口出清的缺陷,证实了使用本文形式化流程可以验证道口控制系统的需求规范并形成可靠的设计原型,从而可提高铁路道口的安全性.(本文来源于《西南交通大学学报》期刊2019年03期）
王戟,詹乃军,冯新宇,刘志明[9]（2019）在《形式化方法概貌》一文中研究指出形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明叁位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明:其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.(本文来源于《软件学报》期刊2019年01期）
王可心[10]（2018）在《软件用例模型形式化方法研究》一文中研究指出本文以在线考试系统的用例模型为主要研究对象,对用例模型描述系统中存在语义模糊等问题进行研究,针对这些存在的问题,提出能够解决其问题的形式化B方法。(本文来源于《中国新通信》期刊2018年22期）
非形式化方法论文开题报告
（1）论文研究背景及目的
此处内容要求：
首先简单简介论文所研究问题的基本概念和背景，再而简单明了地指出论文所要研究解决的具体问题，并提出你的论文准备的观点或解决方法。
写法范例：
近年来,民用航空系统复杂度越来越高,随之而来的是其安全性和可靠性等非功能性需求越来越庞大,造成的结果是难以通过传统的测试方法完成软件功能的全覆盖测试,特别是在复杂逻辑控制领域,如自动驾驶仪、控显等,其状态空间往往超过了1010～1020的规模。在理论层面,对于大规模状态空间,一般采用形式化方法进行数学推演完成穷举测试,但是早期的系统需求和设计往往基于自然语言描述,不具备形式化验证的基础。近年来,随着基于模型的方法在系统和软件领域的推广使用,使得系统或软件逐步具备了半形式化或形式化的描述方式,形式化验证技术也开始随之得到了更广泛的应用。本文以飞行控制模态管理项目为基础,介绍了几个主流形式化验证方法的工程应用及验证结果,说明了该方法在高可靠高安全民用飞行控制领域应用的可行性和实用性。
（2）本文研究方法
调查法：该方法是有目的、有系统的搜集有关研究对象的具体信息。
观察法：用自己的感官和辅助工具直接观察研究对象从而得到有关信息。
实验法：通过主支变革、控制研究对象来发现与确认事物间的因果关系。
文献研究法：通过调查文献来获得资料，从而全面的、正确的了解掌握研究方法。
实证研究法：依据现有的科学理论和实践的需要提出设计。
定性分析法：对研究对象进行“质”的方面的研究，这个方法需要计算的数据较少。
定量分析法：通过具体的数字，使人们对研究对象的认识进一步精确化。
跨学科研究法：运用多学科的理论、方法和成果从整体上对某一课题进行研究。
功能分析法：这是社会科学用来分析社会现象的一种方法，从某一功能出发研究多个方面的影响。
模拟法：通过创设一个与原型相似的模型来间接研究原型某种特性的一种形容方法。
非形式化方法论文参考文献
[1].师新峰.企业内控信息化实施的规范化方法研究——基于领域分析与形式化方法[J].大众投资指南.2019
[2].张丹涛,田贝,张馨洋,朱立平.基于形式化方法进行复杂逻辑系统的验证[C].2019年（第四届）中国航空科学技术大会论文集.2019
[3].马振威,陈钢.基于Coq记录的矩阵形式化方法[J].计算机科学.2019
[4].王陈.基于Event-B形式化方法的免疫系统模型研究[D].扬州大学.2019
[5].陈金凤.形式化方法在自动代码生成中的研究与应用[D].华北电力大学.2019
[6].张维珺.基于形式化方法的系统需求建模与安全性分析研究[D].南京航空航天大学.2019
[7].黄健.携手形式化方法守望计算之春——记上海交通大学电子信息与电气工程学院特别副研究员符鸿飞[J].中国科技奖励.2019
[8].王恪铭,王峥.基于形式化方法的道口控制系统规范建模与验证[J].西南交通大学学报.2019
[9].王戟,詹乃军,冯新宇,刘志明.形式化方法概貌[J].软件学报.2019
[10].王可心.软件用例模型形式化方法研究[J].中国新通信.2018