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

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

Abstract: The complexity of concurrent program verification is uncertain in running, therefore it is difficult to make clear the relation- ship of the verification contents and the verification aim. To resolve the problem, this paper proposes a reliability verification method for concurrent program based on separation logic. It describes an execution diagram about the relation and its statements, turns the logic expression of program property into the logic combination expression of variable concurrent statements sequence, and makes property expression associated with concurrent program statements. It confirms statement execution sequence and logic expression according to logic combination expression, verifies programs according to the expression based on separation logic and temporary logic, and modifies concurrent program by verification result. The Bank counter business function module is implemented based on the proposed verification method, and it shows that the method is effective.

Key words: Hoare logic, separation logic, concurrent program, logic combination expression, reliability verification

中图分类号: 

• TP301