| 发明名称 | 模型检验安全性的参数化线程 | ||
| 摘要 | 用于计算计算机系统的并发程序、例如控制计算机硬件、如磁盘驱动器、音频扬声器等的设备驱动程序中的数据流的系统和方法，包括：给定包括多个类似组件的并发程序，对于并发程序之间的交互初始化(12)可达控制状态集合。基于该可达控制状态集合，去除(14)这些控制状态之间的同步构造。用内部转换取代(14)这些同步构造。添加(16)通过同步构造的去除所揭示的新可达控制状态，其中，使用对单线程的模型检验而查找这些新可达控制状态。通过审查完整的可达控制状态集合来验证(20)上述多个并发程序的数据竞争自由。 | ||
| 申请公布号 | CN101512481B | 申请公布日期 | 2012.05.09 |
| 申请号 | CN200780032884.7 | 申请日期 | 2007.10.04 |
| 申请人 | 美国日本电气实验室公司 | 发明人 | V·卡隆 |
| 分类号 | G06F9/06(2006.01)I | 主分类号 | G06F9/06(2006.01)I |
| 代理机构 | 中国专利代理(香港)有限公司 72001 | 代理人 | 柯广华;李家麟 |
| 主权项 | 一种用于计算计算机系统的并发程序中的数据流的方法，包括：给定多个并发程序，初始化可达控制状态集合；基于所述可达控制状态集合，去除所述控制状态之间的同步构造；用内部转换取代所述同步构造；添加通过所述同步构造的所述去除所揭示的新可达控制状态，其中，利用对单线程的模型检验来发现所述新可达控制状态；以及通过审查完整的可达控制状态集合来验证所述多个并发程序的数据竞争自由。 | ||
| 地址 | 美国新泽西州 | ||