基于隔离逻辑的并行程序可靠性验证方法

摘要：

并行程序验证的复杂性在于执行流程的不确定性以及由此导致的执行规模变大，使得验证的内容和目标之间的关系不明确。为解决该问题，提出一种基于隔离逻辑的并行程序可靠性验证方法。通过变量的执行关系图，描述变量相关的语句及执行关系，将所需验证的程序性质逻辑式转换为变量并行语句序列的逻辑组合式，使得性质表达式与并发程序的语句相关联。根据逻辑组合式确定语句执行序列和前后件逻辑表达式，基于并发隔离逻辑的公理系统对语句执行序列进行验证，并根据验证结果对并发程序进行修改和完善。通过对银行柜台业务办理的功能模块验证结果表明该方法是有效的。

关键词：霍尔逻辑、隔离逻辑、并行程序、逻辑组合式、可靠性验证

分类号：TP301(计算技术、计算机技术)

资助基金：贵州省自然科学基金资助项目J[2011]2328；中央高校基本科研业务费专项基金资助项目12XNLF06

在线出版日期：2014-05-28（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：86-91,96