检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

终止证明方法在形式化建模中的应用

计算机系统应用 2022年第1期31卷 327-331页

作者：任凭张杰关永北京化工大学信息科学与技术学院北京100029 首都师范大学信息工程学院北京100048

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解... 详细信息

随着形式化方法的普及和应用,定理证明器HOL4在形式化建模过程中无法自动完成终止证明的情况越来越多,而手动终止证明又缺少通用的证明思路.针对这种情况,提出规范化的手动终止证明方法.该方法从问题产生的本质入手,首先保证目标具备解决终止问题的必要条件,然后通过等效替换简化证明目标,最后以原有定理库为基础,寻找证明过程中缺失的引理,推进证明.实例表明,该方法逻辑清晰,能够有效地解决HOL4中大部分情况下的手动终止证明问题.

关键词：形式化方法 HOL4 终止证明

在线全文

学校读者我要写书评

暂无评论

一种形式化的组件化软件过程建模方法

软件学报 2011年第1期22卷 1-16页

作者：翟健杨秋松肖俊超李明树中国科学院软件研究所互联网软件技术实验室北京100190 中国科学院研究生院北京100049 中国科学院软件研究所计算机科学国家重点实验室北京100190

为了解决当前软件过程重用方法中存在的问题,特别是由于缺乏对软件过程组件及其操作法则的精确定义所带来的重用中的低效率问题,介绍了一种形式化的组件化软件过程建模方法(componentized software process modeling,简称CSPM).CSPM提... 详细信息

为了解决当前软件过程重用方法中存在的问题,特别是由于缺乏对软件过程组件及其操作法则的精确定义所带来的重用中的低效率问题,介绍了一种形式化的组件化软件过程建模方法(componentized software process modeling,简称CSPM).CSPM提供了形式化定义可重用软件过程的机制,并且给出了将过程组件组合成过程模型的一系列操作法则.利用CSPM方法,能够以严格的方式对软件过程组件进行重用,并且有效地避免了传统非形式化建模方法中因歧义而有可能引起的潜在错误.CSPM还可以将对组装后的软件过程模型针对某些特定性质的验证问题转化成对其对应组件的一系列子验证问题,从而通过指数地减少需要搜索的状态空间规模,将原来在某些特定环境下不实用的验证问题简化成验证代价较小的一系列问题.

关键词：软件过程过程建模过程重用过程组件形式化方法

基于Event-B形式化方法的免疫系统模型研究

在线全文

学校读者我要写书评

暂无评论

基于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方法的免疫系统抽象模型,详细地展示了从需求重写到模型验证的全过程,体现了在软件开发前期使用形式化进行模型验证的重要性。

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

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

形式化方法的理论及其影响

形式化方法的理论及其影响

作者：王祥兵贵州大学

学位级别：硕士

形式化方法是现代逻辑研究的一种基本方法,也是构建现代逻辑理论的框架工具。它本质是一种演绎方法,是人类理性精神的体现和智慧的结晶。本文采用系统科学的全新视角,对形式化方法展开四个层面的研究:①用系统观点考察形式化方法对命题... 详细信息

形式化方法是现代逻辑研究的一种基本方法,也是构建现代逻辑理论的框架工具。它本质是一种演绎方法,是人类理性精神的体现和智慧的结晶。本文采用系统科学的全新视角,对形式化方法展开四个层面的研究:①用系统观点考察形式化方法对命题逻辑和谓词逻辑系统建构和重要理论问题中的应用;②以跨学科、交叉性的研究进路,讨论形式化方法的技术基础--公理化方法的一般性理论和思维范式。③采用逻辑与历史相一致的方法探讨逻辑形式化与数学结构化的发生、发展过程及相互关系问题,并从逻辑史视角探讨形式化方法产生的原动力。④从方法论视角对数学结构主义产生原因、与形式化方法思想渊源进行探讨;并用比较法研究数学结构与形式化的区别与联系。通过以上四个方面对形式化方法的研究阐释清形式化方法在现代逻辑理论与现代数学理论间应用的张力、逻辑形式化与数学结构化的比较与对接、交融与互动关系问题及形式化方法的一般性理论和思维范式等方面有全面、深入的认识,因而无论逻辑科学、数学科学还是逻辑史、数学史的研究都有重要意义。

关键词：形式化方法数学结构主义公理化方法形式系统形式语言

形式化方法在氢氧化铝焙烧炉联锁设计中的应用

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

自动化应用 2015年第5期 41-43页

作者：黄其杨贵阳铝镁设计研究院有限公司贵阳550081

介绍形式化方法的基础知识,及其在氢氧化铝焙烧炉风机系统联锁逻辑设计中的应用。

关键词：形式化方法氢氧化铝焙烧炉联锁设计

在线全文

学校读者我要写书评

暂无评论

形式化方法Designware、B的比较

计算机工程与应用 2007年第31期43卷 96-99页

作者：胡启敏薛锦云江西师范大学瑶湖校区计算机信息工程学院

用形式化方法开发软件是提高软件可靠性和开发效率的革命性途径。Designware、B是两种支持软件开发全过程的形式化方法。对它们的规约描述方法、规约求精方式、开发步骤进行比较,最后分析这两种方法各自的优缺点。

关键词：形式化方法 Designware B方法规约求精

在线全文

学校读者我要写书评

暂无评论

软件形式化方法与应用专题前言

软件学报 2016年第3期27卷 495-496页

作者：詹乃军王戟李宣东计算机科学国家重点实验室(中国科学院软件研究所) 北京100190 国防科学技术大学计算机学院湖南长沙410073 计算机软件新技术国家重点实验室(南京大学) 江苏南京210023

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专... 详细信息

形式化方法起步于程序理论和语义的研究,历经50余年的发展,成为了计算机科学的重要领域.它使用严格的数学方法,研究并发展软件和硬件系统的建模、设计、开发、验证与演化等技术,为保障系统的正确性、可靠性和安全性提供了重要途径.本专题收录的13篇论文反映了近年来我国学者在软件形式化方法与应用领域的部分研究成果.

关键词：形式化方法高阶逻辑应用专题定理证明器程序理论数学方法研究成果代数的计算机科学保障系统

在线全文

学校读者我要写书评

暂无评论

基于形式化需求模型的测试用例生成方法研究

基于形式化需求模型的测试用例生成方法研究

作者：汪文轩南京航空航天大学

学位级别：硕士

航空电子系统软件是一类典型的安全关键性软件,为了保证这类软件系统的安全性,行业内对其开发过程和验证流程做出了非常严格的规定,其中需求的验证和开发是其中最为关键的环节,本文的工作就是在现有工作的基础上,针对D0-178C中的要求,... 详细信息

航空电子系统软件是一类典型的安全关键性软件,为了保证这类软件系统的安全性,行业内对其开发过程和验证流程做出了非常严格的规定,其中需求的验证和开发是其中最为关键的环节,本文的工作就是在现有工作的基础上,针对D0-178C中的要求,为航电软件开发过程中基于需求的测试这一环节提供自动化生成测试用例的支持。从需求模型中获得合适的测试用例集合的关键问题就是从需求模型定义的输入空间中选择一组具有代表性的测试点集合,这个测试点集合必须满足两个要求,即测试点必须对需求模型的需求元素做到良好的覆盖保证测试充分性,在保证这一点的同时应尽量减少测试点的数量以降低测试成本,提高测试可行性。本文工作的核心就是从需求模型平展化、测试路径精简、测试点选择三个阶段逐步来实现这一目标。本文的具体内容如下:(1)本文介绍了航空电子以需求为中心的开发流程,阐述了航空电子系统开发过程中各种以需求为基准的验证活动。解释了用形式化需求模型来对航电系统需求进行建模分析的必要性,以及基于需求模型自动生成测试用例的重要性,并给出了本文工作的基础VRM需求模型的详细定义和建模实例。(2)本文详细阐述了在VRM需求模型的基础上生成测试用例的方法,首先通过对需求模型语义进行解析,给出了对VRM需求模型中各类表格元素的语义解析及平展化的方法。在得到平展化后的测试路径后,提出了一种控制树的数据结构对测试路径进行管理和规约,并根据VRM需求模型的特点,针对Do-178C对于测试覆盖率的要求,提出了三种VRM需求模型测试覆盖率的定义,并此定义的基础上,研究了根据不同的测试覆盖率准则对测试路径进行简化的方法。最后,从工程实践的基础上,提出了针对典型实现错误测试的测试路径内测试点选择方法。(3)介绍了基于本文给出的测试用例自动生成方法为核心而开发出来的一套集成了需求管理及测试用例双向管理、测试用例生成、测试用例辅助设计等功能的工具软件。详细介绍了此工具的功能特性,操作流程,和设计思想。(4)本文以一个较大型的航电软件系统飞行指引系统的模式控制部分展开了实例研究。详细介绍了此系统的实际应用背景,以及相关的需求细节及需求建模。在此系统的需求模型的基础上,展示了通过本文中提出的测试用例生成方法对该需求模型进行用例生成的过程和生成的结果。

关键词：航空电子软件基于需求的测试形式化方法测试用例生成

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

一种基于π演算的行为建模形式化方法

系统工程理论与实践 2009年第5期29卷 175-185页

作者：仲辉王维平黄炎焱李群国防科技大学系统工程系长沙410073

根据人的行为建模形式化方法需求,针对直接应用π演算形式化建模人的行为所存在的不足,尝试以π演算为基础扩展定义了一种人的行为建模形式化方法πr-BFMBM(π-Based Formal Method of Behavioral Modeling);并结合具体示例,阐述了扩展... 详细信息

根据人的行为建模形式化方法需求,针对直接应用π演算形式化建模人的行为所存在的不足,尝试以π演算为基础扩展定义了一种人的行为建模形式化方法πr-BFMBM(π-Based Formal Method of Behavioral Modeling);并结合具体示例,阐述了扩展内容为π-BFMBM方法带来的、增强的行为描述能力及其实现方法.研究表明,相比于π演算,π-BFMBM方法能够为人的行为建模提供更为有力地支持.

关键词：人的行为建模形式化方法 π演算 π-BFMBM