项目简介：带参并发系统广泛存在于各类计算机系统的核心模块中，如操作系统中对共享资源的互斥访问、分布式文件系统的数据一致性控制、多处理器体系下的缓存一致性协议、机场的起飞与降落控制系统等。带参并发系统的每一个具体实例都是有穷状态系统，但却有无穷多个具体实例，因此无法对其进行穷尽的测试、分析或验证。将形式验证方法应用于带参并发系统成为当前的前沿研究课题。 在带参模型检测的理论和算法、验证存储一致性模型技术、带参系统验证工具三个方面取得了一定的成果。在带参模型检测的理论和算法方面，提出了一种结合环境抽象和参数抽象的新方法，并以很小的空间开销把包括FLASH，GERMAN协议都成功完成了验证。这是FLASH这类工业级的复杂协议第一次同时在控制部分和数据部分均得到高度自动化的验证。在验证存储一致性模型技术方面，对龙芯3号多核处理器的存储子系统进行了验证。在带参系统验证工具方面，具有两个验证工具原型。其中PaTLV是一个通用的带参模型检测工具，是世界上少数几个基于启发信息的全自动化的带参模型检测工具。此外，针对存储一致性模型的验证开发了一个存储一致性模型验证工具MOTEC，该工具能够对多种存储一致性模型进行验证。

产品性能：在带参模型检测工具方面，根据软件所的理论研究成果，实现了一个带参模型检测工具PaTLV，该工具以开源工具TLV为基础，能够自动进行辅助不变式的计算和卫士增强，全自动化的进行带参模型检测，包括自动进行系统抽象、自动计算辅助不变式量、自动进行卫士增强等过程。这是世界上少数几个基于启发信息的全自动化的带参模型检测工具。 在存储一致性模型的验证方面，在理论研究的基础上，实现了一个存储一致性模型的验证工具原型MOTEC，该工具通过定期扫描处理器的Performance Counter获得多个指令间的时间约束关系，并利用指令窗口的有界性来降低验证的时间复杂度，能够对多种不同的处理器结构进行验证。图2是MOTEC的一个执行实例。

应用行业：电子与信息

应用范围：系统提出了结合环境抽象和参数抽象的新的带参模型检测方法，在方法的自动化程度以及处理复杂系统的能力方面均取得了进展。形式验证在工业界的应用越来越广泛，对龙芯3号多核处理器的存储子系统进行了验证。 研发的带参并发系统验证工具原型可以用于各种通信协议、网络协议和多核处理器系统的形式验证，具有一定的实用性。