| 一种嵌入式系统扩展流关系Petri网及应用 |
| |
| 引用本文： | 张辉,董荣胜,高西.一种嵌入式系统扩展流关系Petri网及应用[J].广西科学院学报,2007,23(4):254-257. |
| |
| 作者姓名： | 张辉 董荣胜 高西 |
| |
| 作者单位： | 桂林电子科技大学计算机系,广西桂林,541004 |
| |
| 基金项目： | 广西研究生教育计划项目 |
| |
| 摘 要： | 为了将数据流和控制流在同一个模型中明确标识,将经典Petri网的4元组结构扩展为7元组,定义一种新的嵌入式系统扩展流关系Petri网表示方法,应用该表示法对火车控制系统进行建模,并将该模转换成等价的时间自动机模型,用UPPAAL进行形式化验证.验证结果表明火车控制系统具有可达性和安全性,说明建立的模型是合理有效的.
|
| 关 键 词： | Petri网 时间自动机 CTL UPPAAL |
| 文章编号： | 1002-7378（2007）04-0254-04 |
| 收稿时间： | 2007-08-13 |
| 修稿时间： | 2007年8月13日 |
An Extended Flow Petri Net for Embedded Systems and Application |
| |
| ZHANG Hui,DONG Rong-sheng and GAO Xi.An Extended Flow Petri Net for Embedded Systems and Application[J].Journal of Guangxi Academy of Sciences,2007,23(4):254-257. |
| |
| Authors: | ZHANG Hui DONG Rong-sheng and GAO Xi |
| |
| Institution: | Department of Computer Science, Guilin University of Electronic Technology, Guilin, Guangxi, 541004, China,Department of Computer Science, Guilin University of Electronic Technology, Guilin, Guangxi, 541004, China and Department of Computer Science, Guilin University of Electronic Technology, Guilin, Guangxi, 541004, China |
| |
| Abstract: | In order to identify the control flow and data flow in one model,the classical four-tuple structure of Petri net is modified to a seven tuple in this paper.A new extended flow Petri net representation suited to embedded systems is presented.The representation is used to model for railway control system,and the model is translated into timed automata in order to verify the system by UPPAAL.Experimental results show the attainable ability and safety of the railway control system and demonstrate the validity of the model. |
| |
| Keywords: | Petri net timed automaton computation tree logic UPPAAL |
| 本文献已被 维普 万方数据 等数据库收录！ |
| 点击此处可从《广西科学院学报》浏览原始摘要信息 |
| 点击此处可从《广西科学院学报》下载免费的PDF全文 |
|
