检索结果-南通市图书馆

在线全文

学校读者我要写书评

暂无评论

桥梁徐变效应的有限元算法研究及程序验证

铁道标准设计 2022年第11期66卷 62-68页

作者：王雨权廖立坚李林安霍学晋李黎中国铁路设计集团有限公司天津300308 天津大学力学系天津300350 中铁大桥勘测设计院集团有限公司武汉430050 中铁第六勘察设计院集团有限公司天津300308

徐变是控制混凝土桥梁设计的重要因素,但因徐变计算一般封装于商业软件中,设计人员无法掌握计算原理。为研制自主有限元软件,摸索出桥梁徐变计算过程,从徐变系数开始研究,并对Midas帮助文件和基于Tröst-Bazant的工程实用分析算法进行基... 详细信息

徐变是控制混凝土桥梁设计的重要因素,但因徐变计算一般封装于商业软件中,设计人员无法掌握计算原理。为研制自主有限元软件,摸索出桥梁徐变计算过程,从徐变系数开始研究,并对Midas帮助文件和基于Tröst-Bazant的工程实用分析算法进行基于公式推导的对比分析;基于分析结果进一步给出递推形式的徐变累加计算模型,并通过连续梁实例测试验证。研究结果表明:(1)Midas帮助文件给出的徐变算法和基于Tröst-Bazant基本方程的徐变算法本质上是一致的,当满足ρ(t,τ_(0))=1/2时,两者之间的方程是等价的;(2)通过加权最小二乘法将徐变系数写成通用格式,可将基于空间梁单元的徐变算法改造成递推形式,加快运算速度;(3)基于递推形式编制的卧龙程序,在同等边界条件下,其徐变位移的计算精度满足工程设计要求,竖向最大相对误差3%左右,且绝对误差较小,水平向相对误差在1%以内。

关键词：桥梁工程理论分析徐变效应徐变位移递推形式最小二乘法程序验证

基于路径依赖自动机的不变量生成及程序验证方法研究

在线全文

学校读者我要写书评

暂无评论

基于路径依赖自动机的不变量生成及程序验证方法研究

作者：林英文天津大学

学位级别：硕士

在软件开发过程中,如何保证程序的正确性是一个重要问题,其中一种方法就是使用程序验证技术。如何分析和证明程序中的循环是程序验证中的一大难点,使用循环不变量可以证明程序中循环的正确性。然而由于循环的结构复杂,现有不变量生成方... 详细信息

在软件开发过程中,如何保证程序的正确性是一个重要问题,其中一种方法就是使用程序验证技术。如何分析和证明程序中的循环是程序验证中的一大难点,使用循环不变量可以证明程序中循环的正确性。然而由于循环的结构复杂,现有不变量生成方法效率较低并且只能处理部分循环。循环不变量生成问题中的主要难点包括候选不变量的数量较多、循环的结构复杂以及难以验证候选不变量是否有效。因此本文提出了一种新的循环不变量生成方法,此方法使用路径依赖自动机来对循环进行建模,将多路径循环的不变量生成问题转化成了模型中各个状态的状态不变量生成问题。给出了利用路径依赖自动机计算模型中各个状态的约束集合的算法,以及利用约束集合生成状态不变量并最终生成循环不变量的算法。且利用不同的测试集来对此方法进行评估,实验结果表明对于多路径循环来说此方法的效果更好。此外,基于此循环不变量生成方法,本文还提出了利用循环不变量进行程序验证的方法,主要针对程序中断言的正确性和变量是否出现数据溢出两类问题,将这两类验证问题转化成了不变量生成问题。此方法首先通过程序切片来对待分析的程序进行简化,之后尝试利用循环不变量来对程序进行证明,对于无法利用不变量进行证明的程序,通过反例生成算法寻找程序中使断言不满足的路径,以对程序进行证伪。实验结果证明,相比于其他工具本文所提出的方法能够验证更多的程序,尤其是在处理迭代次数较多的循环时效率更高。综上所述,本文基于路径依赖模型提出了一种新的循环不变量生成方法,并将其应用到程序验证中。这是对现有循环分析方法的一种补充,提高了分析多路径循环的效率。

关键词：循环不变量程序验证反例生成程序分析

同方学位论文库评论

在线全文

同方学位论文库

学校读者我要写书评

暂无评论

量子程序验证

软件学报 2018年第4期29卷 1085-1093页

作者：冯元应明生 University of Technology Sydney Australia 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190 清华大学计算机系北京100084

量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5～10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而,由于量子信息的不可克隆性和纠缠的... 详细信息

量子硬件设计与制造技术的飞速发展使得人们开始预言大于100个量子比特的特定用途的量子计算机有望在5～10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键因素.然而,由于量子信息的不可克隆性和纠缠的非局域作用等量子特征,如何设计正确、高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法,特别是模型检测技术,已在经典软件设计和系统建模方面被证明行之有效,因此量子软件的形式化验证也开始受到越来越多的关注.从量子顺序程序验证和量子通信协议验证两方面,对近年来国内外学者,尤其对University of Technology Sydney和清华大学的研究组在该研究领域取得的一些成果进行了系统的总结.最后,对未来可能的研究方向和面临的挑战进行了简单展望.

关键词：量子计算程序验证模型检测通信协议验证

在线全文

学校读者我要写书评

暂无评论

一个程序验证器的设计和实现

计算机研究与发展 2013年第5期50卷 1044-1054页

作者：张志天李兆鹏陈意云刘刚中国科学技术大学计算机科学技术学院合肥230026 中国科学技术大学苏州研究院软件安全实验室江苏苏州215123

形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状... 详细信息

形式验证是提高软件可信程度的重要方法,基于逻辑推理对程序性质进行严格的自动证明是当前的研究热点,但尚无可供工业界使用的产品,其根源在于自动定理证明方面的困难.介绍在通过程序分析建立起各程序点的形状图的基础上,如何利用形状图提供的信息来支持程序验证的方法.提出一种利用形状图信息来消除访问路径别名,使得指针程序中非指针部分的性质仍然可以用Hoare逻辑来进行验证的方法,并证明了该方法的可靠性.还提出一种在不使用自定义谓词的情况下,易变数据结构上数据性质的描述和验证方法.另外,介绍所设计并实现的基于上述方法的PointerC语言的程序验证器的原型.它不仅能自动验证操作易变数据结构程序的性质,也能自动验证使用一维数组的程序的性质.

关键词：程序验证 Hoare逻辑形状图逻辑程序分析分离逻辑

在线全文

学校读者我要写书评

暂无评论

基于SMT求解器的路径敏感程序验证

软件学报 2012年第10期23卷 2655-2664页

作者：何炎祥吴伟陈勇徐超武汉大学计算机学院湖北武汉430072 软件工程国家重点实验室(武汉大学) 湖北武汉430072

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损... 详细信息

随着软件规模的不断扩大以及复杂度的不断增长,人们越来越关注软件的可信性问题.验证程序是否满足断言所描述的性质,是保证软件可信性的一种常见方法.路径敏感的程序验证由于不可能遍历所有的路径,需要合并路径信息,因此造成精度上的损失.提出一种基于SMT求解器的路径敏感程序验证方法,在保证精确度的前提下,有效减少路径搜索空间.其基本思想是,利用最大强连通分量压缩循环路径,然后根据目标断言对控制流图进行切片.使用一种布尔表达式方法对路径空间进行抽象,结合抽象解释和符号执行技术对路径进行验证.结合F-Soft平台和Z3工具对该方法进行了实验验证,结果表明,该方法在验证的精确度和效率上都有较好的效果.

关键词：路径敏感程序验证抽象解释符号执行 SMT求解器

在线全文

学校读者我要写书评

暂无评论

物理质团法关于可压流计算的程序验证

航空动力学报 2019年第6期34卷 1253-1272页

作者：马智博石磊于明郑欢北京应用物理与计算数学研究所北京100094 浙江陆特能源科技股份有限公司杭州310052

为了评估无网格物理质团法(PECM)对可压流计算的可信性,结合物理认识对该方法的设计思想和数值格式进行了先验分析,基于9个一维模型数值解与参照解的对比信息,通过后验分析方法对PECM进行了程序验证,参照解包括无网格再生核粒子法(RKPM... 详细信息

为了评估无网格物理质团法(PECM)对可压流计算的可信性,结合物理认识对该方法的设计思想和数值格式进行了先验分析,基于9个一维模型数值解与参照解的对比信息,通过后验分析方法对PECM进行了程序验证,参照解包括无网格再生核粒子法(RKPM)的数值解以及精确解。验证结果表明:各种物理参数以及状态方程的强烈间断会导致RKPM严重的失稳或失真,而PECM在包括极大密度比在内的各种强间断条件下仍保持稳定和收敛并具有较高的准确度。

关键词：无网格方法物理质团法光滑粒子法再生核粒子法程序验证

在线全文

学校读者我要写书评

暂无评论

基于抽象解释理论的程序验证技术

软件学报 2008年第1期19卷 17-26页

作者：李梦君李舟军陈火旺国防科学技术大学计算机学院湖南长沙410073 北京航空航天大学计算机科学与工程学院北京100083

抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程... 详细信息

抽象解释(abstract interpretation)理论是Cousot.P和Cousot.R于1977年提出的程序静态分析时构造和逼近(approxiamation)程序不动点语义的理论.描述了程序语义基于Galois连接的抽象解释理论框架,讨论了基于抽象解释理论的程序变换、程序安全性验证和活性性质验证这3种典型的应用,并指出了基于抽象解释理论的程序验证的主要研究方向.

关键词：抽象解释理论 Galois连接程序验证

在线全文

学校读者我要写书评

暂无评论

基于分离逻辑的程序验证技术

软件学报 2009年第8期20卷 2051-2061页

作者：黄达明曾庆凯南京大学计算机软件新技术国家重点实验室江苏南京210093 南京大学计算机科学与技术系江苏南京210093

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入... 详细信息

介绍了分离逻辑的验证原理和特点及其在程序验证方面的应用实例,分析了为支持程序验证的若干分离逻辑研究进展,包括分离逻辑的自身属性、与其他逻辑的关系、对程序语言和设计模式的支持以及定理证明器等内容.指出了分离逻辑进一步深入应用所面临的问题和解决方向.

关键词：可信软件程序验证霍尔逻辑分离逻辑定理证明

基于通信Petri网的异步通信程序验证模型

在线全文

学校读者我要写书评

暂无评论

软件学报 2017年第4期28卷 804-818页

作者：杨启哲李国强上海交通大学软件学院上海200240

由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通... 详细信息

由于多栈的模型图灵等价,因此,通用的异步通信程序模型的验证问题不可判定.为此,基于Petri网,提出了一个新的模型通信——通信Petri网,对异步通信程序进行刻画.通过对输入通信进行k-型限制以及对每个栈进行基于正则语言泵引理的抽象,通过将这样限制下的模型编码到数据Petri网,证明了限制下的新模型可覆盖性可判定.

关键词：异步通信程序通信Petri网可覆盖性程序验证 k-型