丁如江, 李国强

(上海交通大学 软件学院,上海 200240)

近年来,基于 Petri网的模型检测技术已经成功地应用于并发程序的验证与分析[1-4]中.Petri网是一种适用于描述并发程序的模型,德国学者Sistla[5]首次提出了使用 Petri网来为程序建模的方法.具体来说,可以用Petri网模型中的位置(place)表示程序的状态,用模型中的迁移(transition)表示程序的执行流,以及每个位置的令牌(token)数表示当前有多少个进程刚好运行到该位置.

并发系统的安全性问题是指系统是否会有可能进入某一错误状态(比如需保证进程互斥的系统发生了多个进程同时运行到某一关键位置),规约到Petri网的可覆盖性问题为:给定一个Petri网和一个状态M(对应到并发系统中的一个错误状态),是否会有一些由初始状态M0可达的状态M′覆盖了M.如果存在可达状态覆盖错误状态M,就表明模型对应的系统不是绝对安全的,系统在理论上会覆盖这个错误状态.现有的验证Petri网可覆盖性的算法大致分为两类:一类是基于Petri网状态空间的遍历,通过搜索Petri网的可达状态空间来判断是否覆盖待验证状态M.然而,由于Petri网的状态空间规模与其位置迁移数是指数级别关系,所以这类算法在面对规模较大的Petri网时都显得力不从心.比如BFC[4]、MIST、IIC[6]等工具都会有超时的问题存在.第2类是基于约束的,从Petri网的模型结构以及待验证状态中提取出约束条件,然后去求解这些约束来验证可覆盖性.然而由于约束的表达能力有限,不可能完美地表达出Petri网……