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

• 作者: 张辉 董荣胜 高西
• 来源期刊: 广西科学院学报
• 学科: 工学
• 关键词: Petri网 时间自动机 CTL UPPAAL
• 年，卷（期）: 2007,（4）
• 页码范围: 254-257
• 页数: 4页
• 分类号: TP301.2
• 字数: 2637字
• 语种: 中文
• DOI: 10.3969/j.issn.1002-7378.2007.04.014

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	张辉	桂林电子科技大学计算机系	5	14	3.0	3.0
2	董荣胜	桂林电子科技大学计算机系	115	1521	13.0	37.0
3	高西	桂林电子科技大学计算机系	4	10	2.0	3.0