Extended Petri Net Based Formal Modeling and Verification of WTB-TCN Device

被引：0

作者：

Liu, Ming ^{[1
]}

Zhang, Guoyin ^{[1
]}

Yao, Aihong ^{[1
]}

机构：

[1] Harbin Engn Univ Harbin, Coll Comp Sci & Technol, Harbin, Peoples R China

来源：

PROCEEDINGS OF 2010 3RD IEEE INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE AND INFORMATION TECHNOLOGY (ICCSIT 2010), VOL 8 | 2010年

关键词：

formal verification; Petri net; model checking; WTB-TCN; embeded system;

D O I：

暂无

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

This paper presents a formal methodology of modeling and verification about WTB-TCN device based on extended Petri net model. By translating the model into timed automata, properties of WTB-TCN device can be completely verified using symbolic model checking technique. The methodology proposed addresses the model checking of critical properties of WTB-TCN device including safety, Iiveness and fairness properties which are expressed in computation tree logics. As a confirmation of its validity, the methodology described in this paper has been successfully applied to modeling and formal verification of WTB-TCN device.

引用

页码：110 / 114

页数：5

共 10 条

[1] A THEORY OF TIMED AUTOMATA [J].

ALUR, R ;

DILL, DL .

THEORETICAL COMPUTER SCIENCE, 1994, 126 (02) :183-235

[2] A link-layer slave device design of the MVB-TCN bus (IEC 61375 and IEEE 1473-T) [J].

Carlos Moreno, Juan ;

Laloya, Eduardo ;

Navarro, Jesus .

IEEE TRANSACTIONS ON VEHICULAR TECHNOLOGY, 2007, 56 (06) :3457-3468

[3]

Jensen K., 1994, Decade of Concurrency. Reflections and Perspectives. REX School/Symposium Proceedings, P230

[4]

Ming L., HIERARCHICAL R UNPUB

[5]

Mitra RS, 2008, DES AUT CON, P800

[6] Line redundancy in MVB-TCN devices: A control unit design [J].

Moreno, Juan Carlos ;

Laloya, Eduardo Jesus ;

Navarro, Jesus .

CIRCUITS AND SYSTEMS FOR SIGNAL PROCESSING , INFORMATION AND COMMUNICATION TECHNOLOGIES, AND POWER SOURCES AND SYSTEMS, VOL 1 AND 2, PROCEEDINGS, 2006, :789-794

[7]

Roig O, 1995, LECT NOTES COMPUT SC, V935, P374

[8]

Schäfers C, 2000, 2000 IEEE 51ST VEHICULAR TECHNOLOGY CONFERENCE, PROCEEDINGS, VOLS 1-3, P1581, DOI 10.1109/VETECS.2000.851393

[9]

Verstoep K, 2009, INT PARALL DISTRIB P, P201

[10]

Yamada C, 2007, ELE COM ENG, P208

← 1 →