图搜索问题算法推导及形式化证明

用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.     

3个变形背包问题的形式化推导

在对0-1背包问题的若干变形问题进行深入研究的基础上,使用二进制数组的方式形式化描述了几种背包问题的程序规约,通过程序规约变换技术获取问题求解的递推关系,给出了3个变形背包问题的算法推导过程,有效保证了算法程序的可靠性,并可将采用的推导方法在子集和问题、船装载等问题中加以推广应用.     

分划递推法在Hanoi塔问题上的应用

采用分划递推法通过功能归约变换,形式化推导和证明Hanoi塔问题中圆盘的移动规律,从而推导出结构清晰、可读性好、效率高、占用存储空间与圆盘个数无关的非递归算法,算法比较分析地显示出形式化推导在获得高效和正确性的算法程序中的作用.相关算法在UNIX平台下用C语言进行实现.     

二叉树排序非递归算法推导及形式化证明

非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.     

二叉树队列关系问题非递归算法的推导及形式化证明

该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递...     

形式化开发若干组合数学问题的算法

计算机科学的核心内容是使用算法处理离散数据,组合数学的重要性日渐凸显.使用形式化方法PAR开发了两个组合数学问题的算法,形式化推导过程为问题求解提供了思路,自然地引进了算法程序中用到的变量,清晰地展示了算法程序的设计过程,最终可得到简洁、易理解、可靠性高的算法程序.对形式化方法开发组合算法做了积极的探索,有利于促进组合算法设计自动化的研究及形式化开发方法的推广应用.     

模型驱动的Dafny程序形式化生成与自动验证

Dafny是一种内置规范结构的编程语言和静态程序证明器,它能验证程序的功能正确性以及将证明过程自动化,这既提高了软件开发的效率,又极大增强了软件开发的可靠性.该文探索了一种模型驱动的Dafny程序形式化生成的方法.首先,从问题的Radl规约出发,根据规约变换技术得到其Radl算法; 然后,根据PAR方法中循环不变式开发新策略得到问题的循环不变式; 最后,在Radl算法和循环不变式基础上利用模型等价转换规则生成Dafny程序,并由Dafny证明器自动验证其功能正确性.用该方法解决了2个典型问题的算法程序开发与验证,证实了该方法能够有效地提高Dafny程序的生成效率和可靠性.     

基于Apla语言的虚拟现实建模机制研究

针对传统的脚本建模存在语言机制复杂繁琐、开发效率不高、可靠性难保证、建模阶段和交互阶段相互独立等问题,基于分划与递推(PAR)及其Apla抽象程序设计语言,设计与原Apla语言融合的虚拟现实建模语言机制。开发的Apla→MAXScript自动生成系统可以将抽象Apla程序转换成MAXScript脚本,并借助3DSMax来实现三维建模。Apla建模机制采用直接重用MAXScript修改器API方式,既大幅度简化了重构的工作量,又延续了Apla语言抽象程度高特征,便于对Apla建模程序进行形式化推导和正确性验证。最后通过案例证明了Apla建模语言及其工具能够提高三维建模的精细度、可靠性及开发效率。     

一种验证软件演化过程行为的代数推导方法

针对现有软件过程验证主要以结构验证和性质验证为主,缺乏行为验证的不足,提出了一种验证软件演化过程行为的代数方法.该方法使用通信进程代数ACP对软件演化过程元模型EPMM进行扩展,提出软件演化过程元模型代数EPMM-A.针对EPMM建模产生的软件演化过程模型,一方面使用EPMM-A形式定义软件演化过程模型的行为规约,另一方面在其公理系统的支持下,基于等式推导验证软件演化过程模型的行为与行为规约是否一致,使行为验证方式从模型推导(非形式化)变为代数推导(形式化).为了说明代数推导的正确性,证明了软件演化过程元模型代数的公理系统具有可靠性.     

树非递归遍历统一的新解法及其形式证明

提出树遍历统一的新解法,使其非递归算法像递归算法一样简单.首先以后序遍历为例,基于结点状态标记和遍历规则提取,从遍历定义导出遍历的递推公式,由此机械获得非递归算法和循环不变式,并用形式化方法证明其正确性.之后按不同遍历定义变换公式参数,获得二叉树前序、中序和K叉树前序、后序的递推公式,所得算法比传统算法更简洁直观,表明本解法的有效性和通用性.     

PLC程序形式化的设计与验证

从形式化方法的角度出发,阐述可编程逻辑控制器(PLC)程序的形式化设计和验证方法的相关研究.在形式化设计方面,分析了根据Petri网和自动机模型判断程序正确性和可靠性的研究成果;在形式化验证方面,分析了PLC语言与形式化模型的转换和基于NuSMV或UPPAAL的验证方法.最后,比较将两种形式化方法应用到PLC程序的特点,探讨现有成果中存在的问题及研究发展方向.     

一个描述FOXPRO汇总程序的形式化方法

对于ＦＯＸＰＲＯ语言设计的汇总程序，本文提出一个用于描述其正确性的形式化方法，作为示例，文中最后对汇总程序的核心部分给出了部分正确性验证过程。     

一种基于Concurrent Apla语言的共享内存并发分布式算法2层验证方法

形式化验证共享内存并发分布式算法已成为当前极具挑战性的问题之一,尤其是在云计算、多核、无线传感器网络、分布式数据库、区块链环境下.该文基于研究团队在形式化规约语言和方法、算法形式推导和验证方面的已有工作,以自定义泛型抽象顺序设计语言Apla为基础,进一步研究并提出简明、高抽象用于并发分布式计算的Concurrent Apla语言,使其既支持顺序算法的验证又能有效地验证并发分布式算法.在依赖-卫式推理的基础上,提出一种新颖的2层并发分布式算法形式化验证方法,其中系统层用于处理并发级验证,而组件层用于处理顺序级验证.最后,通过2个实例验证了该方法的有效性和可行性.     

VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究

形式化方法是保证操作系统设计和实现的正确性的可靠方法.操作系统的形式化设计和验证过程仍然是一个极其复杂的过程.由于汇编语言过于底层,对其进行形式化验证的难度较大,如何有效地对汇编语言代码进行建模,便于对其语义和功效的正确性进行验证成为操作系统形式化领域的研究热点.在汇编级提出对操作系统的设计和实现的正确性进行形式化验证的方法.通过建立操作系统内核硬件抽象模型,形式化地描述指令的操作语义,在此内核硬件抽象模型的基础上界定影响系统状态变化的数据对象,建立系统状态空间,结合指令的操作语义的定义来描述系统的状态转换函数.在Isabelle/HOL定理证明器环境中描述该内核硬件抽象模型,以实现的可信操作系统VSOS为例,在汇编级对系统设计和实现的正确性进行验证.结果表明,该方法是可行的和高效的.     

基于SPIN的BPEL4WS建模与验证研究

Web服务组合研究领域的一个重要问题是如何形式化描述Web服务组合,验证服务组合的正确性,Web服务组合的形式化模型可以用来检查和验证Web服务组合以保证组合的正确性.文章使用模型检查工具SPIN对目前普遍使用的Web服务组合规范BPEL4WS (Business Process Execution Language for Web Services,Web服务业务流程执行语言)模型进行了验证,给出了BPEL4WS语法到Promela形式化模型的转换方法,最后通过一个实例对BPEL4WS表示的服务组合模型的安全性、活性和有界性等特性进行了验证分析,从而给出了基于SPIN的BPEL4WS表示的Web服务组合模型验证的方法.     

基于超图文法的软件体系结构动态演化

提出用带约束的超图表示软件体系结构,给出基于超图态射的软件体系结构动态演化通用产生式规则的形式化语义和操作,定义类型超图作为体系结构风格,运用超图文法和体系结构风格建模软件体系结构动态演化.为了验证软件体系结构动态演化的正确性,采用模型检测技术,设计算法对软件体系结构动态演化性质进行形式化验证,并应用模型检测工具进行实验分析.该方法既提供了图形化的直观表示,又展示了基于文法的形式化理论框架.     

基于GOERTZEL算法的双音多频信号检测与仿真

本文首先介绍了双音多频的概念、存在的问题以及双音多频信号产生的原理,然后推导了双音多频信号检测中的DFT算法和GOERTZEL算法。最后设计了基于GOERTZEL算法的MATLAB检测程序,得出相应的频谱图,并对仿真结果的正确性进行了验证。     

一种航空电子系统体系结构错误行为验证方法

针对航空电子系统体系结构安全性评估过程中,组件故障影响分析,正确性难以保证的问题,提出了一种基于模型的体系结构错误行为描述和验证方法。首先,针对系统功能需求和安全性目标,建立体系结构模型;然后,采用错误模型附件描述组件的错误行为和导致的故障影响,并使用层次自动机作为中间状态,通过转换算法实现体系结构错误行为模型的形式化描述;最后,通过模型检测实现安全性需求的正确性验证。实例分析表明,该方法能够验证体系结构设计的组件错误影响和应对措施是否满足系统的安全性目标,提升安全性评估的准确性和效率。     

一种用于循环程序形式化验证的划分归纳方法

为了提高软件的可靠性,人们一直在形式化验证和软件测试两个方面进行不懈的努力.本文利用划分测试中的自动分割替代技术,针对循环程序的输入域,提出了一种划分算法,并在此算法的结果上建立一种划分归纳方法,它能简化循环程序的形式化验证过程.     

2类数列问题循环不变式开发策略研究与应用

该文通过对组合数学中Catalan数列问题和Fibonacci数列问题进行深入研究,利用归纳推理、组合数学中的加法和乘法原理等方法得到问题求解函数,使用变量记录算法求解过程中子问题的解,并约束循环变量的变化范围,获得问题求解算法的循环不变式,由此得到了2类数列问题循环不变式的统一开发策略.以二叉树的形态数问题和阶梯问题为例,利用所提策略开发循环不变式,并基于循环不变式展示了这2类数列问题算法程序的形式化推导过程.