基于上下文定界的并发程序验证技术研究

摘要

随着多核计算的兴起，并发软件成为计算机辅助验证的重要目标。并发软件系统在社会生活、国民经济等诸多关键领域的应用愈加普遍，软件系统存在的微小错误或漏洞可能会引起重大的经济损失甚至难以预计的后果，检测软件缺陷的形式化验证技术成为学术界和工业界备受关注的热点。
　　近年来，大型并发软件系统普遍采用任务驱动或者事件驱动的编程方法，本文的研究重点是针对并发程序的形式化验证技术，通过对其抽象模型进行高效的可达性分析，确定抽象模型是否满足预期的性质或者规格。可达性分析是一种常见的程序验证技术，通过搜索程序执行产生的状态空间，确定程序是否会到达某些错误的状态，从而查找程序中的错误或漏洞。论文针对并发程序的可达性分析进行研究，取得如下创新成果：
　　1.针对Fork/Join并行模式的并发程序的可达性问题进行分析，将可以模拟Fork/Join并行线程创建的并发程序执行的抽象模型（动态并发下推系统）化简为对应的并发下推系统，化简后的系统可以使用现有的k-定界可达算法进行求解。
　　2.采用上下文定界方法抑制状态空间爆炸问题，通过约束系统进程的消息队列是良序的，证明其上下文切换定界可达性问题是可判定的。提出一种构造模拟递归队列并发程序执行的多栈下推系统的转换方法，将其上下文切换定界可达性问题转换为多栈下推系统的阶定界可达性问题。
　　3.基于上下文定界思想和良序排队约束，提出一种针对多栈下推系统的上下文切换定界可达算法，对下推系统迭代地应用标准Post*算法，穷尽地计算k次上下文切换内正向可达的格局，通过对目标状态集合与可达格局集合的交集进行判空，最终解决递归队列并发程序的可达性问题。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

§1.1 研究背景与意义

§1.2 国内外研究现状

§1.3 研究内容与主要贡献

§1.4 论文结构

第二章 模型检验与自动机理论

§2.1 模型检验技术概述

§2.2自动机理论

§2.3可达性问题

§2.4 结束语

第三章 并发程序

§3.1 并发程序简介

§3.2 事件驱动架构

§3.3 基于队列通信的并发递归程序

§3.4 结束语

第四章 Fork/Join并行性的并发程序可达性分析

§4.1 抽象模型

§4.2 定界可达问题描述

§4.3 k-定界可达算法

§4.4 基于上下文定界的可达性分析

§4.5 本章小结

第五章 基于队列通信的并发递归程序可达性分析

§5.1 抽象模型

§5.2 递归程序转换为多栈下推系统

§5.3 k-上下文切换定界可达算法

§5.4 实例分析

§5.5 本章小结

第六章 结束与展望

§6.1 主要研究工作

§6.2 下一步待研究的问题

参考文献

致谢

作者在攻读硕士期间主要研究成果