| 引用本文： |
-
张辉,董荣胜,高西.一种嵌入式系统扩展流关系Petri网及应用[J].广西科学院学报,2007,23(4):254-257. [点击复制]
- ZHANG Hui,DONG Rong-sheng,GAO Xi.An Extended Flow Petri Net for Embedded Systems and Application[J].Journal of Guangxi Academy of Sciences,2007,23(4):254-257. [点击复制]
|
|
| 摘要: |
| 为了将数据流和控制流在同一个模型中明确标识,将经典Petri网的4元组结构扩展为7元组,定义一种新的嵌入式系统扩展流关系Petri网表示方法,应用该表示法对火车控制系统进行建模,并将该模转换成等价的时间自动机模型,用UPPAAL进行形式化验证。验证结果表明火车控制系统具有可达性和安全性,说明建立的模型是合理有效的。 |
| 关键词: Petri网 时间自动机 CTL UPPAAL |
| DOI： |
| 投稿时间：2007-08-13 |
| 基金项目:广西研究生教育计划项目(2007105950812M17)资助 |
|
| An Extended Flow Petri Net for Embedded Systems and Application |
|
ZHANG Hui, DONG Rong-sheng, GAO Xi
|
| (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. |
| Key words: Petri net timed automaton computation tree logic UPPAAL |
