欢迎来到喀斯玛汇智科技服务平台

服务热线: 010-82648522

首页 > 成果推荐 > 成果详情
带参并发系统的形式验证方法

带参并发系统的形式验证方法


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

  • 我要咨询
官方客服(周一至周五:8:30-17:30) 010-82648522