基于抽象和符号技术的并发软件验证研究

形式化验证是国际计算机科学基础研究的前沿领域之一，其中并发软件的验证是当前形式化验证的重点及难点。模型检验并发软件的主要难点是组合状态空间爆炸问题。本项目将以并发C程序为研究对象，使用抽象和符号技术，缩减局部和全局状态空间。基于抽象解释和完备域构造理论，研究并发程序性质强保留的最优完备抽象；采用抽象解释的特殊形式- - 谓词抽象，研究依赖验证公式的最优性质弱保留抽象，从而获得并发布尔程序；研究并发布尔程序的紧凑符号表示及线程计数器抽象的符号算法；基于上下文限界k，采用Lazy策略分析并发可达性到顺序可达性，并通过高效的符号算法来验证并发布尔程序。研究对布尔程序进行限界模型检验及基于SAT的抽象反例精化问题，以及限界模型检验问题转化为ASP（Answer set programming）问题，通过对逻辑程序的解集计算，从而完成验证，并设计基于ASP限界模型检验的高效算法，具有学术上的创新性。

随着多核计算的发展，并发软件在计算机辅助验证领域中已成为重要研究目标。软件模型检验的难点是组合状态空间爆炸问题，抽象是解决状态空间爆炸的重要方法。首先系统地构造演算L语义模型的安全抽象，并在此基础上，变换为通用Kripke结构下的安全抽象。然后基于抽象解释框架，以及完备抽象解释和性质强保留之间的关系，构造使得L性质强保留的最小抽象模型精化，并转换为抽象解释中抽象域的最小完备精化。依据此完备抽象域求得性质强保留的最优抽象状态划分，从而构造出性质强保留且最优的抽象状态转换系统。.当模型包含递归过程调用时，即使仅考虑执行有限次上下文切换，其可达性问题仍是不可判定的。假定进程的消息队列约束为良序，则其在上下文切换定界上的可达性为可判定。首先提出构造能模拟递归队列并发程序执行的多栈下推系统的转换方法；然后给出一种基于多栈下推系统的上下文切换定界可达算法，算法使用标准Post*操作描述下推系统的迭代，基于良序排队控制进程对队列的出队操作，穷尽地计算k次上下文切换内的正向可达格局；最后对目标状态集合与可达格局状态集合的交集进行判空，确定目标状态是否可达，从而较好地解决此类并发程序的可达性问题。.当前的CSP模型检测需将进程转化为迁移系统进行提取语义模型，转化过程比较复杂；其性质采用CSP语言进行规范，有利于精炼检测方式，但通用性不强，描述能力较弱。鉴于此，提出了一种基于mini-trace的CSP模型检测方法，其中mini-trace模型采用迹语义的递归策略来计算，性质采用LTL进行规范；并证明了基于mini-trace模型验证的可靠性。利用ASP实现了mini-trace模型的自动生成机制以及LTL的自动验证机制，并集成了一个CSP检测系统—T_ASP。实验表明，与类似系统相比，该系统的描述能力更强，验证结果的准确性更高，且可同时验证多条性质，在性质不满足时还可提供多条反例。.利用π演算能有效建模移动并发系统的特征，借鉴程序语言中不同类型变量之间的赋值方式，提出基于混杂类型检测的安全π演算πHTS。根据πHTS利用静态类型检测保障低机密级信息只能向同等或更高机密级流动，高完整级信息只能向同等或更低完整级流动，针对机密性和完整性在信息流向上的相反性，提出了基于强制类型转化的有效动态转换框架。πHTS将静态检测和动态检测有机地整合在一起，形成了一种统一的安全形式模型。