基于隔离逻辑的并行程序可靠性验证方法
外文标题：Reliability Verification Method for Concurrent Program Based on Separation Logic
文献类型：期刊
作者：万良[1]
机构：中国人民大学信息学院，北京 100872; 中国人民大学数据工程与知识工程教育部重点实验室，北京 100872; 贵州大学计算机科学与技术学院，贵阳 550025
年：2014
期刊名称：计算机工程
卷：40
期：2
页码范围：86-91,96
增刊：增刊
收录情况：中国科技核心期刊
所属部门：信息学院；数据工程与知识工程教育部重点实验室
语言：中文
ISSN：1000-3428
链接地址：http://d.g.wanfangdata.com.cn/Periodical_jsjgc201402019.aspx
DOI：10.3969/j.issn.1000-3428.2014.02.019
人气指数：8
浏览次数：8
基金：贵州省自然科学基金资助项目(J[2011]2328)；中央高校基本科研业务费专项基金资助项目
关键词：霍尔逻辑;隔离逻辑;并行程序;逻辑组合式;可靠性验证
摘要：并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大，使得验证的内容和目标之间的关系不明确。为解决该问题，提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图，描述变量相关的语句及执行关系，将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式，使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式，基于并发隔离逻辑的公理系统对语句执行序列进行验证，并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。
作者其他论文
磁盘阵列环境下的取证目标系统重构.杨勇;石文昌;梁彬,等.计算机应用与软件.2014,64-67,74.
基于分离逻辑的并行程序性质验证方法.万良;石文昌;冯慧.计算机科学.2013,40(10),148-154.
一种安全转移系统模型的构造及其运用.万良;肖源.计算机应用研究.2014,31(2),558-562.
基于TCT的取证工具适应性问题及其解决方法研究.翟皓昊;石文昌;梁彬,等.计算机应用与软件.2012,8-11.
