A PROTOCOL MODELING AND VERIFICATION APPROACH BASED ON A SPECIFICATION LANGUAGE AND PETRI NETS

被引：16

作者：

SUZUKI, T ^{[1
]}

SHATZ, SM ^{[1
]}

MURATA, T ^{[1
]}

机构：

[1] UNIV ILLINOIS, DEPT ELECT ENGN & COMP SCI, CHICAGO, IL 60680 USA

来源：

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING | 1990年 / 16卷 / 05期

基金：

美国国家科学基金会;

关键词：

Petri nets; protocols; specification; verification;

D O I：

10.1109/32.52775

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

An approach for automated modeling and verification of communication protocols is presented. A language that specifies input/ output behavior of protocol entities is introduced as the starting point of the approach and verification of the linguistic specifications is discussed. Rules for conversion of the specifications into a Petri net model (based on a timed Petri net) are presented and illustrated by examples. This leads to a second level of verification on the net model. The approach is illustrated by its application to a part of the LAPD protocol. © 1990, IEEE.

引用

页码：523 / 536

页数：14

共 50 条

[21] Modular verification of Petri Nets properties:: A structure-based approach
Klai, K
Haddad, S
Ilié, JM
[J]. FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2005, 2005, 3731 : 189 - 203
[22] Modeling and Verification of SCTP Association Management Based on Timed Colored Petri Nets
Zhang, Shengcai
An, Dezhi
Wu, Guangli
[J]. 2016 2ND IEEE INTERNATIONAL CONFERENCE ON COMPUTER AND COMMUNICATIONS (ICCC), 2016, : 2090 - 2093
[23] A Petri nets-based approach to modeling SCORM sequence
Lin, HW
Shih, TK
Chang, WC
Yang, CH
Wang, CC
[J]. 2004 IEEE INTERNATIONAL CONFERENCE ON MULTIMEDIA AND EXP (ICME), VOLS 1-3, 2004, : 1247 - 1250
[24] VERIFICATION OF SPECIFICATIONS WRITTEN IN THE ESTELLE LANGUAGE USING PETRI NETS
DIMITROV, V
PETKOV, A
[J]. AVTOMATIKA I VYCHISLITELNAYA TEKHNIKA, 1989, (05): : 23 - 27
[25] PNets - the Verification Tool based on Petri Nets
Siebert, Miroslav
Flochova, Jana
[J]. WORLD CONGRESS ON ENGINEERING - WCE 2013, VOL I, 2013, : 369 - 373
[26] MODULAR VERIFICATION OF PETRI NETS - THE TEMPORAL LOGIC APPROACH
DAMM, W
DOHMEN, G
GERSTNER, V
JOSKO, B
[J]. LECTURE NOTES IN COMPUTER SCIENCE, 1990, 430 : 180 - 207
[27] VERIFICATION OF ERROR RECOVERY SPECIFICATION FOR DISTRIBUTED DATA BY USING COLORED PETRI NETS
AKATSU, M
MURATA, T
KURIHARA, K
[J]. IEICE TRANSACTIONS ON COMMUNICATIONS ELECTRONICS INFORMATION AND SYSTEMS, 1991, 74 (10): : 3159 - 3167
[28] A compositional approach to the specification of multimedia objects using Petri nets
Anisimov, NA
Kovalenko, AA
Postupalski, PA
Vuong, ST
[J]. FIRST ANNUAL CONFERENCE ON EMERGING TECHNOLOGIES AND APPLICATIONS IN COMMUNICATIONS, PROCEEDINGS, 1996, : 38 - 41
[29] Petri nets model of unified modeling language statecharts
Guo, Feng
[J]. Jisuanji Jicheng Zhizao Xitong/Computer Integrated Manufacturing Systems, CIMS, 2007, 13 (07): : 1300 - 1307
[30] Modeling and verification of sequential control paths using Petri nets
Erhard, W
Reinsch, A
Schober, T
[J]. DESDES '1: PROCEEDINGS OF THE INTERNATIONAL WORKSHOP ON DISCRETE-EVENT SYSTEM DESIGN, 2001, : 41 - 46

← 1 2 3 4 5 →