中文会议： 广西计算机学会2007年年会论文集

会议日期： 2007-10-01

会议地点： 南宁

主办单位： 广西计算机学会

作　　者： ; ; ;

机构地区： 桂林电子科技大学计算机科学与工程学院计算机科学与技术系

出　　处： 《广西计算机学会2007年年会》

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

关 键 词： 火车控制系统 网 时间自动机 嵌入式系统

分 类 号： [TP]

领　　域： [自动化与计算机技术]