期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
共找到5篇文章
< 1 >
每页显示 20 50 100
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
显示方式：
基于交互式定理证明的并发程序验证工作综述
1
作者 王中烨 吴姝姝 曹钦翔 《软件学报》 EI CSCD 北大核心 2024年第9期4069-4099,共31页
并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定... 并发程序与并发系统可以拥有非常高的执行效率和相对串行系统较快的响应速度,在现实中有着非常广泛的应用.但是并发程序与并发系统往往难以保证其实现的正确性,实际应用程序运行中的错误会带来严重的后果.同时,并发程序执行时的不确定性会给其正确性验证带来巨大的困难.在形式化验证方法中,人们可以通过交互式定理证明器严格地对并发程序进行验证.对在交互式定理证明中可用于描述并发程序正确性的验证目标进行总结,它们包括霍尔三元组、可线性化、上下文精化和逻辑原子性.交互式定理证明方法中常用程序逻辑对程序进行验证,分析基于并发分离逻辑、依赖保证逻辑、关系霍尔逻辑等理论研究的系列成果与相应形式化方案,并对使用这些方法的程序验证工具和程序验证成果进行总结. 展开更多
关键词 并发程序验证 可线性化 上下文精化 程序逻辑 关系霍尔逻辑
下载PDF
基于隔离逻辑的并行程序可靠性验证方法 被引量：2
2
作者 万良 《计算机工程》 CAS CSCD 2014年第2期86-91,96,共7页
并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,... 并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大,使得验证的内容和目标之间的关系不明确。为解决该问题,提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图,描述变量相关的语句及执行关系,将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式,使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式,基于并发隔离逻辑的公理系统对语句执行序列进行验证,并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。 展开更多
关键词 霍尔逻辑 隔离逻辑 并行程序 逻辑组合式 可靠性验证
下载PDF
基于无干扰理论的并发程序隐私性分析模型研究 被引量：1
3
作者 曹珲 张焕国 严飞 《武汉大学学报（理学版）》 CAS CSCD 北大核心 2012年第6期508-514,共7页
基于无干扰理论和Hoare公理方法,针对并发进程中不可信代码带来的信息泄露问题,提出一种隐私性分析模型CPNIAM,一方面把并发程序功能正确性证明分化为对程序中所有并发进程的形式化验证,以达到复杂程序简单化证明的目的;另一方面,可以... 基于无干扰理论和Hoare公理方法,针对并发进程中不可信代码带来的信息泄露问题,提出一种隐私性分析模型CPNIAM,一方面把并发程序功能正确性证明分化为对程序中所有并发进程的形式化验证,以达到复杂程序简单化证明的目的;另一方面,可以在进程的功能正确性验证的基础上进行并发进程间的无干扰性分析.实例分析表明,相对于传统的无干扰模型,本文提出的模型可以在程序设计及实现阶段的形式化验证过程中,对由不可信代码导致的进程间隐私泄露问题进行分析,分析结果可指导程序设计者用于不可信代码定位和修改. 展开更多
关键词 隐私保护 无干扰理论 Hoare公理方法 并发程序 形式化验证
原文传递
基于分离逻辑的云存储系统并发正确性验证
4
作者 王子豪 王捍贫 《广州大学学报（自然科学版）》 CAS 2022年第3期14-28,共15页
云存储系统的应用日益广泛,其可靠性尤为受研究者关注。现有的基于块分离逻辑的验证方法能很好地描述和验证具备“文件-块-数据”三层架构的云存储系统的各类性质,文章在此基础上提出一种验证云存储系统并发正确性的方法,工作包括:(1)... 云存储系统的应用日益广泛,其可靠性尤为受研究者关注。现有的基于块分离逻辑的验证方法能很好地描述和验证具备“文件-块-数据”三层架构的云存储系统的各类性质,文章在此基础上提出一种验证云存储系统并发正确性的方法,工作包括:(1)扩展云存储系统的建模语言,增加对线程间通信等并发行为的描述;(2)扩展断言语言,用于描述云存储环境下与并发执行和存储控制相关的系统性质;(3)提出一组霍尔规则,用于推导系统的性质。文章给出的验证实例能说明该方法的有效性。文章的工作扩展了块分离逻辑的适用范围,为MapReduce等框架下的并发程序正确性验证工作提供了理论基础。 展开更多
关键词 分离逻辑 并发程序验证 云存储系统
下载PDF
基于TL2软件事务内存的并发程序的精化验证
5
作者 赵立飞 《电子技术（上海）》 2014年第9期43-49,共7页
软件事务内存并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者,从而大大减轻高层程序员开发并发程序的负担。TL2是一个经典的基于锁的高性能软件事务内存算法。本文以一个TL2读写事务的底层具体实现为验证目标,首先采用并... 软件事务内存并发机制将对共享存储复杂的同步访问控制转嫁给底层系统开发者,从而大大减轻高层程序员开发并发程序的负担。TL2是一个经典的基于锁的高性能软件事务内存算法。本文以一个TL2读写事务的底层具体实现为验证目标,首先采用并发程序间的精化关系来刻画基于TL2的底层细粒度并发程序是某个具体的高层抽象原子事务代码块的正确实现,然后通过基于依赖保证的并发程序模拟技术证明两个程序间具有精化关系,完成读写事务的底层实现在代码级的验证并总结TL2算法满足的不变式,为完成TL2算法在代码级的完整验证奠定基础。 展开更多
关键词 软件事务内存 并发程序验证 TL2 基于依赖保证的模拟技术 精化验证
原文传递
已选择0条
导出题录 引用分析
参考文献
引证文献
 统计分析
检索结果
已选文献
上一页 1 下一页 到第 页
使用帮助 返回顶部