期刊文献+
共找到39篇文章
< 1 2 >
每页显示 20 50 100
基于Isabelle定理证明器算法程序的形式化验证 被引量:9
1
作者 游珍 薛锦云 《计算机工程与科学》 CSCD 北大核心 2009年第10期85-89,共5页
形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序... 形式化验证对保证软件的正确性和可靠性具有十分重要的意义。定理机械证明是形式化验证的一个重要研究领域,Isabelle系统是一个被广泛运用的定理证明辅助工具。本文在分析Dijkstra最弱前置谓词理论的基础上,根据PAR方法开发的算法程序循环不变式,提出了一种使用Isabelle定理证明器对算法程序进行机械验证的方法。该方法既克服了传统手工验证过程的繁琐性和易错性等缺点,又达到"提高验证效率和保证算法程序高可信"的目标,具有很好的实用价值。 展开更多
关键词 形式化验证 定理机械证明 Dijkstra最弱前置谓词理论 PAR方法 算法程序 定理证明器
下载PDF
若干算法程序的形式化推导与生成技术研究 被引量:7
2
作者 胡启敏 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2008年第z1期148-153,共6页
PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于... PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序. 展开更多
关键词 PAR方法 形式化推导 算法程序 递推关系
下载PDF
基于问题模式的形式化软件规格说明生成方法 被引量:5
3
作者 王昌晶 罗海梅 左正康 《计算机研究与发展》 EI CSCD 北大核心 2013年第2期352-360,共9页
精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式... 精确的形式化软件规格说明是软件描述、开发与验证的基础,而工业界普遍使用非(半)形式化的表示定义与描述用户需求,如何由非(半)形式化的用户需求生成形式化软件规格说明是需求工程的难点之一.将设计模式的概念进行扩展,定义了问题模式,提出了一种基于问题模式形式化软件规格说明生成方法.该方法从结构化自然语言SNL描述的高层问题需求出发,通过选择知识库中的问题模式逐步精化得到各个新的子问题对应的形式化规格说明,之后对各个子问题组合并进行优化以得到最终的形式化规格说明.进一步,使用模型精化演算的原理与概念给出了该生成方法的理论基础.采用算法程序领域作为研究对象并使用Radl语言作为形式化规格说明语言.通过算法程序领域中的典型实例对这一方法进行了详细的描述,实际效果表明该方法能有效地生成高质量形式化规格说明. 展开更多
关键词 形式化软件规格说明 生成方法 问题模式 模型精化演算 算法程序
下载PDF
IAPWS-IF97水和水蒸汽热力性质计算程序的研制 被引量:4
4
作者 赵金峰 吴立峰 +1 位作者 张荣欣 李勇 《东北电力大学学报》 2008年第1期32-35,共4页
根据国际水和水蒸汽性质协会(IAPWS)在1997年推出的一系列新的公式,简称为IAPWS- IF97公式,同时针对比焓.比熵子程序计算过程的复杂性,提出了用黄金分割法搜索压力的算法,建立了一个已知比焓.比熵求解压力的数学模型,进行水和水蒸气热... 根据国际水和水蒸汽性质协会(IAPWS)在1997年推出的一系列新的公式,简称为IAPWS- IF97公式,同时针对比焓.比熵子程序计算过程的复杂性,提出了用黄金分割法搜索压力的算法,建立了一个已知比焓.比熵求解压力的数学模型,进行水和水蒸气热力性质计算程序的研制。该程序的计算精度能完全满足实际工程中的需要,且在实际应用中未发现有不收敛点。 展开更多
关键词 水蒸汽性质 黄金分割法 计算程序
下载PDF
基于DIC方法的残余应力快速测量系统 被引量:3
5
作者 宋秋 李晓星 杨岩峰 《实验力学》 CSCD 北大核心 2017年第4期506-516,共11页
结合数字图像相关(Digital Image Correlation,DIC)方法与钻孔法,开发了残余应力快速测量系统。该系统可分为两部分:适用于现场测量的便携式机械系统与针对残余应力测量而改进的基于DIC算法的程序。在四点弯曲加载平台上对工件进行载荷... 结合数字图像相关(Digital Image Correlation,DIC)方法与钻孔法,开发了残余应力快速测量系统。该系统可分为两部分:适用于现场测量的便携式机械系统与针对残余应力测量而改进的基于DIC算法的程序。在四点弯曲加载平台上对工件进行载荷释放前后的残余应力测量试验,通过与应变片测量结果进行对比,该残余应力测量系统的精度达到了应变片测量的同等精度。同时,该测量系统解决了传统应变片测量系统对心误差大、操作繁琐、效率低和测量结果稳定性差等问题,具有较高的工程应用价值。 展开更多
关键词 数字图像相关 钻孔法 残余应力 机械系统 算法程序
原文传递
形式化PAR方法及其算法程序规约精化机理 被引量:1
6
作者 苏昭 《江西科技学院学报》 2014年第3期53-57,共5页
用形式化方法开发软件是提高软件生产效率和可靠性的革命性途径,是实现软件自动化的决定性关键。文章介绍了一种新的支持作为软件开发核心的算法设计的形式化方法PAR,分析了其理论基础及算法程序规约精化机理,并结合一个经典实例开发展... 用形式化方法开发软件是提高软件生产效率和可靠性的革命性途径,是实现软件自动化的决定性关键。文章介绍了一种新的支持作为软件开发核心的算法设计的形式化方法PAR,分析了其理论基础及算法程序规约精化机理,并结合一个经典实例开发展示了PAR的具体使用,给出PAR的实际应用项目,最后对PAR进行了评述。 展开更多
关键词 形式化PAR方法 规约精化 算法程序
下载PDF
一种抽象算法程序到可执行程序的转换
7
作者 胡芳 《电脑知识与技术(过刊)》 2010年第9X期7413-7414,共2页
算法程序是用抽象程序设计语言或可执行的程序设计语言描述的算法。开发正确而有效的算法程序一直是计算机界的核心问题。分划—递推法(PAR方法)是一种统一的算法程序开发方法,采用这种方法开发的算法程序Apla程序是一种抽象算法程序,... 算法程序是用抽象程序设计语言或可执行的程序设计语言描述的算法。开发正确而有效的算法程序一直是计算机界的核心问题。分划—递推法(PAR方法)是一种统一的算法程序开发方法,采用这种方法开发的算法程序Apla程序是一种抽象算法程序,它的每一步都经过严格的数学推导,因而可以保证算法的正确性,采用程序转换技术将抽象算法程序转换为各种执行程序,可以大幅度提高算法程序的效率和可靠性。 展开更多
关键词 算法程序 抽象程序设计语言 程序转换
下载PDF
A Unified Approach for Developing EfficientAlgorithmic Programs 被引量:48
8
作者 薛锦云 《Journal of Computer Science & Technology》 SCIE EI CSCD 1997年第4期314-329,共16页
A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented. An algorithm (represented by recurrence and initiation) is separated from program, and special att... A unified approach called partition-and-recur for developing efficient and correct algorithmic programs is presented. An algorithm (represented by recurrence and initiation) is separated from program, and special attention is paid to algorithm manipulation rather than program calculus. An algorithm is exactly a set of mathematical formulae. It is easier for formal derivation and proof. After getting efficient and correct algorithm, a trivial transformation is used to get a final program. The approach covers several known algorithm design techniques, e.g. dynamic programming, greedy, divide-and-conquer and enumeration, etc. The techniques of partition and recurrence are not new. Partition is a general approach for dealing with complicated objects and is typically used in divide-and-conquer approach. Recurrence is used in algorithm analysis, in developing loop invariants and dynamic programming approach. The main contribution is combining two techniques used in typical algorithm development into a unified and systematic approach to develop general efficient algorithmic programs and presenting a new representation of algorithm that is easier for understanding and demonstrating the correctness and ingenuity of algorithmic programs. 展开更多
关键词 programming method algorithm design method correctness of algorithmic program recurrence relation loop invariant.
原文传递
算法程序形式化开发研究 被引量:10
9
作者 薛锦云 《云南大学学报(自然科学版)》 CAS CSCD 1997年第S2期23-28,共6页
从哲学理论和算法程序开发实践两方面阐述了以演绎推理为基础的算法程序形式化开发的作用和固有局限性,指出排斥算法程序形式化和对形式化方法寄予不切实际的希望都是错误的,主张努力探索算法程序开发的科学基础,使开发中尽可能多的... 从哲学理论和算法程序开发实践两方面阐述了以演绎推理为基础的算法程序形式化开发的作用和固有局限性,指出排斥算法程序形式化和对形式化方法寄予不切实际的希望都是错误的,主张努力探索算法程序开发的科学基础,使开发中尽可能多的创造性劳动,转变为非创造性劳动,才能达到算法程序开发形式化,进而实现自动化的宏伟目标.最后以实例说明了我们提出的算法程序设计和证明的分划递推法为基础,进行算法程序形式化开发的可能性. 展开更多
关键词 算法程序开发方法 演绎推理 创造性劳动 科学基础 形式化方法
原文传递
算法程序变换研究与进展 被引量:3
10
作者 石海鹤 石海鹏 +1 位作者 郑宇军 薛锦云 《计算机科学》 CSCD 北大核心 2007年第11期232-238,共7页
开发算法程序是计算机科学领域中最具挑战性的问题之一。为了提高算法程序的可靠性和生产效率,人们正在追求其开发的自动化。算法程序变换是实现算法程序开发自动化的重要途径,已成为程序设计方法学和软件自动化领域中的重要课题,目前... 开发算法程序是计算机科学领域中最具挑战性的问题之一。为了提高算法程序的可靠性和生产效率,人们正在追求其开发的自动化。算法程序变换是实现算法程序开发自动化的重要途径,已成为程序设计方法学和软件自动化领域中的重要课题,目前已取得很大进展。本文介绍了算法程序变换的相关概念,给出了算法程序变换的分类,并从方法学、语言、算法设计能力、支撑工具及其适用领域等方面分析和比较了几个有代表性的算法程序变换研究项目,讨论了当前研究的不足以及今后的研究方向。 展开更多
关键词 算法程序变换 自动化 形式化方法 算法设计
下载PDF
一组基于PAR的高可靠查找算法程序开发 被引量:2
11
作者 石海鹤 薛锦云 《计算机研究与发展》 EI CSCD 北大核心 2010年第S1期204-208,共5页
使用形式化方法PAR,从查找问题的形式化规约出发,使用量词的性质等作为规则,分别施行不同的等价规约变换,开发了一组查找算法程序,并借助PAR平台进一步将其转换成可执行程序,这清晰展示了各算法程序间存在的关系,保证了结果程序的正确... 使用形式化方法PAR,从查找问题的形式化规约出发,使用量词的性质等作为规则,分别施行不同的等价规约变换,开发了一组查找算法程序,并借助PAR平台进一步将其转换成可执行程序,这清晰展示了各算法程序间存在的关系,保证了结果程序的正确性和可靠性,使得算法程序的设计效率得到提高. 展开更多
关键词 查找算法程序 形式化方法PAR 可靠性
下载PDF
复杂算法程序的规范证明和形式推导 被引量:1
12
作者 薛锦云 《江西师范大学学报(自然科学版)》 CAS 1992年第3期195-202,共8页
能否实现复杂算法程序的规范证明和形式推导是检验某种形式化方法有无生命力的重要标志。本文介绍了这一领域的研究现状,重点综述了作者近年来提出的复杂算法程序形式化技术,以典型实例说明了使用这些技术的方法。
关键词 算法程序 形式化 算法设计
下载PDF
分布式光伏电源的配电网故障特征计算模型分析 被引量:6
13
作者 俞晓峰 袁岭 +3 位作者 崔艺林 钟永城 蓝伟军 曾丁 《粘接》 CAS 2023年第1期140-143,共4页
针对传统故障计算方法存在的计算量大、计算时间长等问题,采用建立含分布式光伏电源配电网故障特征计算模型的方式,维持配电网的稳定运行。利用PQ控制策略对并网型光伏电源进行控制,结合故障分量叠加原理对配电网的故障特征进行分析可知... 针对传统故障计算方法存在的计算量大、计算时间长等问题,采用建立含分布式光伏电源配电网故障特征计算模型的方式,维持配电网的稳定运行。利用PQ控制策略对并网型光伏电源进行控制,结合故障分量叠加原理对配电网的故障特征进行分析可知,负序及零序等值网络中存在的光伏电源接入点没有注入电流;这表明光伏电源模型对改进前推回代算法的收敛性没有影响。以支路角度作为主要依据,形成一种新的配电网故障算法,该算法具有计算效率高、影响较小等优势,有利于提升故障特征的计算效率。 展开更多
关键词 分布式光伏电源 配电网故障特征 改进前推回代算法 算法程序
下载PDF
PCA-BP算法模块化设计的编程实现 被引量:3
14
作者 贾群 《计算机技术与发展》 2008年第12期98-101,105,共5页
BP算法存在收敛性慢、逼近精度差等缺点。因此,在实际应用中往往需要对BP算法进行相应的改进。利用主元分析法(PCA)对数据样本预先进行降维处理,消除数据间的强耦合性,减少模型的复杂性,然后再作为BP的输入样本从而提高模型的解算速度... BP算法存在收敛性慢、逼近精度差等缺点。因此,在实际应用中往往需要对BP算法进行相应的改进。利用主元分析法(PCA)对数据样本预先进行降维处理,消除数据间的强耦合性,减少模型的复杂性,然后再作为BP的输入样本从而提高模型的解算速度。在此分析的基础上利用Visual Basic采用模块化的设计方法实现对PCA-BP算法的编程,使学习速率能够进行相应自调整和优化,以此来提高BP网络的泛化推广能力,并能够满足设定的误差精度从而达到现场实际运用需要的目的。 展开更多
关键词 BP PCA—BP算法 算法编程
下载PDF
核电厂DCS系统逻辑算法在线维护技术研究 被引量:3
15
作者 黄俊 钟科 +1 位作者 马宇 杨斐 《南华大学学报(自然科学版)》 2019年第5期84-89,共6页
在核电厂DCS系统中,算法程序主要完成系统的业务功能,它的可靠性正确性对于整个系统的安全运行具有重要意义。在DCS系统中,算法程序作为主控程序的一部分运行。为了让算法程序运行的每一步均可见,就要对算法产生的所有变量进行维护,其... 在核电厂DCS系统中,算法程序主要完成系统的业务功能,它的可靠性正确性对于整个系统的安全运行具有重要意义。在DCS系统中,算法程序作为主控程序的一部分运行。为了让算法程序运行的每一步均可见,就要对算法产生的所有变量进行维护,其中监控算法程序的内部变量是监控整个算法的关键环节。针对核电厂安全级DCS系统的算法软件安全性需求及内部变量对外不可见的特性,设计了一套算法程序内部变量维护的方法。利用该方法一方面可以实现对整个算法程序运行全过程所有环节的维护功能;另一方面屏蔽了操作人员在处理算法过程中主观因素的介入。这一方法能有效提升用户使用体验,具有可观的经济效益。 展开更多
关键词 DCS系统 算法程序 安全性 在线维护
下载PDF
自动驾驶传感器筛选与优化配置程序研究 被引量:1
16
作者 朱明哲 刘保光 +1 位作者 李柏林 郑广州 《汽车实用技术》 2020年第7期46-47,51,共3页
自动驾驶传感器配置需求随着汽车智能化和电动化的快速发展不断增加。基于当前自动驾驶传感器配置无有效筛选途径的现状,通过建立数据库、设定指标项、制定评判准则和选定算法程序快速实现传感器配置方案匹配,并采用响应曲面算法进行优... 自动驾驶传感器配置需求随着汽车智能化和电动化的快速发展不断增加。基于当前自动驾驶传感器配置无有效筛选途径的现状,通过建立数据库、设定指标项、制定评判准则和选定算法程序快速实现传感器配置方案匹配,并采用响应曲面算法进行优化筛选,满足用户传感器配置需求。 展开更多
关键词 自动驾驶 传感器配置方案 优化筛选 算法程序
下载PDF
基于原-对偶内点法的化工过程优化算法 被引量:1
17
作者 洪伟荣 王彦 谭鹏程 《化工学报》 EI CAS CSCD 北大核心 2010年第8期1978-1982,共5页
在基于积极集SQP的拟序贯算法研究基础上,提出了基于原-对偶内点法的拟序贯化工过程优化算法。拟序贯算法分为模拟层和优化计算层双层。模拟层中使用正交配置法同时离散状态变量和控制变量,变量的边界约束加于配置点上。同时,每次NLP迭... 在基于积极集SQP的拟序贯算法研究基础上,提出了基于原-对偶内点法的拟序贯化工过程优化算法。拟序贯算法分为模拟层和优化计算层双层。模拟层中使用正交配置法同时离散状态变量和控制变量,变量的边界约束加于配置点上。同时,每次NLP迭代均求解离散DAE系统,消除等式约束和状态变量,从而减小NLP问题的规模。最新研究表明,在大规模优化问题中内点法相对于积极集SQP算法具有明显优势,因此,优化计算层中用原-对偶内点法来求解NLP问题。使用FORTRAN语言独立编写了整个算法程序,并通过热集成精馏系统最优控制的动态优化问题验证了算法的有效性。结果显示,该算法具有求解大规模动态优化问题的能力。 展开更多
关键词 化工过程优化 拟序贯算法 原-对偶内点法 算法程序
下载PDF
PCA-BP算法在DMF微量水工艺中的应用
18
作者 贾群 《工业控制计算机》 2008年第9期49-50,共2页
建立PCA-BP模型可以克服BP算法收敛较慢的特点,样本数据经过PCA处理后,维数被大大降低,其收敛性、逼近精度等可以达到工程应用的需要。利用PCA对数据样本预先进行降维处理,消除数据间的强耦合性,然后再作为BP的输入样本。在分析的基础上... 建立PCA-BP模型可以克服BP算法收敛较慢的特点,样本数据经过PCA处理后,维数被大大降低,其收敛性、逼近精度等可以达到工程应用的需要。利用PCA对数据样本预先进行降维处理,消除数据间的强耦合性,然后再作为BP的输入样本。在分析的基础上,利用Visual Basic实现PCA-BP算法编程,以达到进行实际应用的目的。 展开更多
关键词 BP PCA-BP算法 VB算法编程
下载PDF
线性混合强化三维宏微观双尺度弹塑性模型及分析
19
作者 周江贝 孙秦 陈先民 《机械强度》 CAS CSCD 北大核心 2018年第4期852-856,共5页
宏微观双尺度弹塑性模型通过宏微观联系因子获得微观尺度上的塑性应变,它是探讨高周疲劳损伤累积及其破坏机理的有效理论方法。基于双尺度弹塑性模型基本理论,研究了宏观载荷作用下具有塑性强化机制的微观应力应变演变规律,编写程序算... 宏微观双尺度弹塑性模型通过宏微观联系因子获得微观尺度上的塑性应变,它是探讨高周疲劳损伤累积及其破坏机理的有效理论方法。基于双尺度弹塑性模型基本理论,研究了宏观载荷作用下具有塑性强化机制的微观应力应变演变规律,编写程序算法实现了比例混合塑性强化微观应力应变滞回曲线的求解。利用有限元软件Abaqus建立了三维实体模型,通过弹塑性分析获得相应的应力应变及其等效应力应变滞回曲线。对比有限元与本文算法结果,验证并校核了双尺度模型算法的有效性。 展开更多
关键词 宏微观双尺度模型 线性混合塑性强化 有限元模型 算法程序 滞回曲线
下载PDF
模糊自整定PID算法在伺服控制中的应用研究 被引量:9
20
作者 高泽东 李建军 +2 位作者 高教波 王军 解俊虎 《自动化仪表》 CAS 北大核心 2011年第10期55-59,共5页
模糊自整定PID算法的控制系统同时具有PID控制和模糊控制的优点,可满足伺服电机随动控制的高性能跟踪任务需求。基于模糊自整定PID控制原理和模糊控制的基本概念,研究了PID参数模糊自整定模糊化、模糊推理、清晰化这三个步骤的任务内容... 模糊自整定PID算法的控制系统同时具有PID控制和模糊控制的优点,可满足伺服电机随动控制的高性能跟踪任务需求。基于模糊自整定PID控制原理和模糊控制的基本概念,研究了PID参数模糊自整定模糊化、模糊推理、清晰化这三个步骤的任务内容、实现方法和程序函数,并设计了基于该算法的实时伺服控制软件。试验结果表明,基于该算法的伺服控制系统在不同跟踪速度下均具有较高的控制精度和良好的动态性能。 展开更多
关键词 模糊控制 PID控制 伺服控制 实时控制 自整定 算法程序
下载PDF
上一页 1 2 下一页 到第
使用帮助 返回顶部