一种嵌入式系统扩展流关系Petri网及应用

为了将数据流和控制流在同一个模型中明确标识,将经典Petri嗣的4元组结构扩展为7元组,定义一 种新的嵌A式系统扩展流关系Petri同表示方法,应用该表示法对火车控制系统进行建模,并将该模转换成等 价的时间自动机模型.用UPPAAL进行形式化验证。验证结果表明火车控制系统具有可达性和安全性,说明 建立的模型是台理有效的。