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