位置：成果数据库 > 期刊 > 期刊详情页
基于形式演算和不变式验证的可信算法程序构造(英文)
  • ISSN号：1673-5447
  • 期刊名称：《中国通信：英文版》
  • 时间：0
  • 分类：TN[电子电信]
  • 作者机构：[1]College of Computer Science & Technology, [2]Zhejiang University of Technology, [3]Provincial Lab of High-Performance Computing Technology, [4]Jiangxi Normal University
  • 相关基金：National Natural Science Foundation of China under Grant No. 60773054,60870002 and 61020106009; Zhejiang Provincial Natural Science Foundation of China under Grant No. R1110679
作者： 郑宇军[1], 石海鹤[2], 薛锦云[3], 陈胜勇[4]
关键词： FORMAL, methods, algorithm, CALCULATION, LOOP, INVARIANTS, PROGRAM, VALIDATION
中文摘要：

The paper presents a formal and practical approach to dependable algorithm development.First,starting from a formal specification based on the Eindhoven quantifier notation,a problem is regularly reduced to subproblems with less complexity by using a concise set of calculation rules,the result of which establishes a recurrence-based algorithm.Second,a loop invariant is derived from the problem specification and recurrence,which certifies the transformation from the recurrence-based algorithm to one or more ...

英文摘要：

The paper presents a formal and practical approach to dependable algorithm development. First, starting from a formal specification based on the Eindhoven quantifier notation, a problem is regu-larly reduced to subproblems with less complexity by using a concise set of calculation rules, the result of which establishes a recurrence-based algorithm. Second, a loop invariant is derived from the problem specification and recurrence, which certifies the transformation from the recurrence-based algorithm to one or more iterative programs. We demonstrate that our approach covers a number of classical al-gorithm design tactics, develops algorithmic pro-grams together with their proof of correctness, and thus contributes fundamentally to the dependability of computer software.

同期刊论文项目
若干软件新技术及其在PAR平台中的实验研究
期刊论文 49 会议论文 7 获奖 4 著作 3
基于PAR平台的信息系统应用软件若干共性关键技术研究
期刊论文 36 会议论文 20 获奖 6
　机器人自主视觉行为规划和复杂环境三维建模
期刊论文 9
基于领域唯一性彩色编码的实时三维视觉方法研究
期刊论文 106 会议论文 5 获奖 8
同项目期刊论文
Velocity Consistency Analysis for Selecting Excellent Feature Points in Three-Dimensional Reconstruc
Active vision in robotic systems: A survey of recent developments[机器人主动视觉的研究发展，2011年9月被下载/阅读次数最多]
Complete 3D Modeling from Rotational Devices
柔性体点分布模型的时变插值算法
Acceleration Strategies in Generalized Belief Propagation[广义置信度传播的加速算法（比原来加速200倍左右）]
Intelligent Lighting Control for Vision-Based Robotic Manipulation[视觉机器人系统的智能光照控制]
基于单幅光模板的高分辨率可靠3维形貌重建
Kalman Filter for Robot Vision: a Survey[卡尔曼滤波器在机器视觉中的应用]
Determination of Stripe Edge Blurring for Depth Sensing[一种边界模糊程度计算方法及用于深度感知]
One-Shot Optical 3D Sensor by Projection of a Hexagonally Encoded Multicolor Array
基于LCD和KNNCH分类算法的齿轮故障诊断方法
归一化复域能量算子解调及其在转子碰摩故障诊断中的应用
基于多尺度线调频基信号稀疏分解的信号分离和瞬时频率估计
基于SVD和线调频小波路径追踪的转速波动齿轮箱故障诊断
基于MCSSD的转子碰摩故障早期检测
基于稀疏信号分解的自适应时变滤波器及其在齿轮故障诊断中的应用
基于多尺度线调频基稀疏信号分解的广义解调方法及其在齿轮故障诊断中的应用
一种基于多尺度线调频基的稀疏信号分解方法
基于多尺度线调频基稀疏信号分解的包络解调方法及其在齿轮故障诊断中的应用
齿轮箱故障振动信号的阶比多尺度形态学解调
μ-SVD降噪算法及其在齿轮故障诊断中的应用
基于噪声辅助分析的总体局部均值分解方法
转向工况下车辆主动悬架的侧倾控制
面向设备维护联盟的知识安全管理研究
基于局部特征尺度分解的经验包络解调方法及其在机械故障诊断中的应用
局部特征尺度分解方法及其分解能力研究
基于局部特征尺度分解和核最近邻凸包分类算法的滚动轴承故障诊断方法
局部特征尺度分解方法及其分量判据研究
VPMCD和改进ITD的联合智能诊断方法研究
基于多尺度线调频基稀疏信号分解的齿轮故障信号阶比分析
一种抛物面摄像机系统的标定方法
人体心脏的4维图像建模和参数分析
考虑人因可靠性的RCM方法改进研究
Solving Linear Coupled Fractional Differential Equations by Direct Operational Method and Some Appli
The Specular Exponent as a Criterion for Appearance Quality Assessment of Pearl-Like Objects by Arti
Parametric Shape Representation by a Deformable NURBS Model for Cardiac Functional Measurements[基于可变
Detection and amendment of shape distortions based on moment invariants for active shape models, [基于
Tangential Stress Analysis of Myocardial Wall Based on FEM
Optimal Feature Matching for 3D Reconstruction by Combination of Global and Local Information
Key Issues in Modeling of Complex 3D Structures from Video Sequences
Elman Fuzzy Adaptive Control for Obstacle Avoidance of Mobile Robots using Hybrid Force/Position Inc
Myocardial Motion Analysis for Determination of Tei-Index of Human Heart
Modeling of Biological Intelligence for SCM System Optimization
Recent Advances in Morphological Cell Image Analysis
Markov models for image labeling
Non-uniform Simplification of Point Clouds
Formal Calculation and Invariant-Based Validation Establish Dependable Algorithmic Programs
局部特征尺度分解方法及其在齿轮故障诊断中的应用
多目标优化在新车型总体轻量化设计中的应用
板簧后悬架垂直刚度影响因素的研究
Taguchi设计方法和有限元分析方法在车门系统设计中的应用
基于试验设计的某微型客车悬架参数匹配优化
悬架与助力转向系统集成控制建模与仿真
田口鲁棒设计用于汽车动力总成悬置系统
虚拟场景中起重机运动仿真技术研究与应用
基于影响系数法的薄板电阻点焊定位点优化
基于OSEK／VDXNM的汽车舒适性控制系统网络管理的研究
回归分析方法在汽车侧撞安全性设计中的应用
基于EMD与BP神经网络的汽车关门声品质预测
综合考虑解耦率和隔振率的发动机悬置系统多目标优化
采用响应面法的汽车转向系统固有频率优化
基于改进二次粒子群算法的汽车零配件配载优化
基于正交试验设计的微型轿车侧撞安全性研究
田口鲁棒设计方法在汽车耐撞性优化中的应用
两挡变速器纯电动汽车动力性经济性双目标的传动比优化
基于虚拟试验场的汽车车身T型接头疲劳分析
基于Kriging模型的汽车前部结构的耐撞性优化
基于6σ稳健性的拼焊板车门轻量化研究
汽车关门声品质改进方法的研究
多学科优化设计在拼焊板车门轻量化中的应用
基于模态振型的自由阻尼层厚度分布优化
声学数值计算的有限元-最小二乘点插值法
基于遗传蚁群融合算法的超弹性材料参数识别
发动机激励引起的车内结构噪声研究
往复式压缩机吸气消声器设计
区间响应面悬置固有频率匹配研究
自适应滤波在车用发电机噪声测试中的应用
汽车关门声品质评价参数的建立
基于四维图像的心室应力应变分析
线调频小波路径追踪算法和FrFT相结合的升降速齿轮故障诊断方法
基于自适应时变滤波阶比跟踪的齿轮箱故障诊断
二维声学数值计算的径向插值有限元法
基于可靠性的混合不确定参数汽车盘式制动器振动稳定性分析
基于伪WIGNER-VILLE分布的汽车关门声品质评价参数研究
基于壳单元的侧碰移动可变形壁障研究
菱形新概念车制动过程中方向稳定性分析
功能梯度材料飞轮转子优化设计
基于最优控制理论的储能飞轮转子形状优化设计研究
基于响应面法的汽车盘式制动器稳定性优化设计
基于模态振型形状优化的结构声辐射控制
有源噪声控制次级声源的非线性建模
多材料—多零件规格组合结构多目标优化的应用
基于有限元法的模糊参数二维声场数值分析
Tangential stress analysis of myocardial wall by finite element method
Unified categorical models for three typical resource allocation problems
Constraint verification of generic algorithmic program for solving general network path problems
Radl形式规格说明相对正确性研究
PAR 平台数据库查询优化方案
基于 PAR 的软件服务外包开发过程应用研究
A Formal Approach to Critical Components in Disaster Management Information Systems
Research on automated sorting algorithms generation based on PAR
基于PAR的软件服务外包开发过程应用研究
PAR平台数据库查询优化方案
SRLtoRadl生成系统及其范畴论语义
Radl算法到Apla程序的生成系统
一类单元赋值语句型循环不变式的开发方法研究
基于BPMN的Web服务并发交互机制
Fuzzy Combinatorial Optimization With Multiple Ranking Criteria:A Staged Tabu Search Faramework，，201
A new particle swarm optimization algorithm for fuzzy optimization of armored vehicle scheme design
基于主从粒子群模型的分布式Agent计算框架
Biogeographic harmony search for emergency air transportation
Emergency railway transportation planning usinga hyperheuristic approach
An Algebraic Approach to Population-Based Evolutionary Algorithm Generation
Apla中泛型约束机制研究
Disaster rescue task scheduling: An evolutionary multiobjective optimization approach.
Water wave optimization: A new nature-inspiredmetaheuristic
Evolutionary optimization for disaster relief operations: A survey
The forgetting mechanism in Dirichlet reputation system
Apla语言中并发分布式机制的研究
基于PAR的排序算法自动生成研究
Rescue Wings: Mobile Computing and Active ServicesSupport for Disaster Rescue
Transaction在PAR平台中的实现方法及应用研究
软件形式化开发关键部件选取的水波优化方法
多Agent 主从粒子群分布式计算框架
在建模语言Apla中实现多媒体数据库应用的方法研究
Apla→Java程序生成系统中泛型机制实现方法研究
组合优化问题简约与算法推演
基于PAR的软件服务外包开发过程应用研究
PAR平台数据库查询优化方案
形式化方法在高中算法教学中的应用研究
A problem reduction based approach to discrete optimization algorithm design
三个经典数学问题的形式化开发
循环不变式开发技术研究
Huffman算法程序的形式化推导
后序遍历二叉树非递归算法的推导及形式化证明
Towards Semi-Automatic Generation of Provably Correct Algorithmic Programs
基于软件体系结构的可复用构件模型
关系代数派生算子语义表达式间等价性证明
软件测试在APLA→JAVA系统中的应用研究
若干算法程序的形式化推导与生成技术研究
泛型编程扩展及其JAVA实现
Formal analysis of cryptographic protocols in a knowledge algorithm logic framework
Knowledge-Based Support for Object-Oriented Software Design and Synthesis: a category theoretic appr
基于MSET的框架变化点实例化模式挖掘
一类0-1背包问题算法程序的形式化推导
基于SPEC#的功能性冗余软件开发
基于扩展的构件依赖关系图聚类的体系结构重构策略研究
基于PAR的算法形式化开发
装备维修规划的多目标优化模型和求解算法
并行遗传算法骨架的研究和实现
一组基于PAR的高可靠查找算法程序开发
数据驱动的多Agent装备器材保障决策支持系统
多核集群系统上的混合编程模型研究
XML在并行骨架描述中的应用
调频发射机的Wince驱动设计
Approach of generating parallel programs from parallelized algorithm design strategies
网格编程方法与环境综述
柔性体点分布模型的时变插值算法
人体心脏的4维图像建模和参数分析
基于局部匹配窗口的动作识别方法
基于可变形运动模型和运动片元的多角色运动合成
基于流形学习的人体动作识别
多Agent 主从粒子群分布式计算框架
基于蜂窝的多角色交互性动画合成
Human-inspired lighting the intention control in robot systems with of glare avoidance
期刊信息
  • 《中国通信：英文版》
  • 中国科技核心期刊
  • 主管单位:中国科学技术协会
  • 主办单位:中国通信学会
  • 主编：刘复利
  • 地址：北京市东城区广渠门内大街80号6层608
  • 邮编：100062
  • 邮箱：editor@ezcom.cn
  • 电话：010-64553845
  • 国际标准刊号：ISSN：1673-5447
  • 国内统一刊号：ISSN：11-5439/TN
  • 邮发代号:2-539
  • 获奖情况:
  • 国内外数据库收录:
  • 被引量:187