Verification of Estelle-Specified Communication Protocols Using High-Level Petri Nets

被引：0
|
作者：
V. A. Nepomniaschy
G. I. Alekseev
A. V. Bystrov
S. P. Myl'nikov
E. V. Okunishnikova
P. A. Chubarev
T. G. Churina
机构：
[1] Russian Academy of Sciences,Ershov Institute of Information Systems, Siberian Division
来源：
Programming and Computer Software | 2001年 / 27卷
关键词：
Operating System; Artificial Intelligence; Communication Protocol; Program Complex; Semantic Error;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
Estelle specifications are considered that include certain dynamic constructs. A method of translation of these specifications into modified colored Petri nets is described. Static Estelle specifications are translated into hierarchical typed time nets (HTT nets), which are extensions of safe colored Petri nets through the introduction of the notions of time, priorities, and places (which are queues of tokens). A program complex EPV is presented that is designed for verification of static Estelle specifications of communication protocols by translating them into HTT nets. Experiments are described on simulation and search for semantic errors in protocols used in practice.
引用
收藏
页码：58 / 68
页数：10
相关论文
共 50 条
  • [21] Branching processes of high-level Petri nets
    Khomenko, V
    Koutny, M
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 458 - 472
  • [22] SYSTEM MODELING WITH HIGH-LEVEL PETRI NETS
    GENRICH, HJ
    LAUTENBACH, K
    [J]. THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) : 109 - 136
  • [23] A methodology of testing high-level Petri nets
    Zhu, H
    He, XD
    [J]. INFORMATION AND SOFTWARE TECHNOLOGY, 2002, 44 (08) : 473 - 489
  • [24] STOCHASTIC HIGH-LEVEL PETRI NETS AND APPLICATIONS
    LIN, CA
    MARINESCU, DC
    [J]. IEEE TRANSACTIONS ON COMPUTERS, 1988, 37 (07) : 815 - 825
  • [25] CONFLICT HANDLING IN HIGH-LEVEL PETRI NETS
    JAVOR, A
    VIGH, A
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1993, 39 (2-5): : 133 - 136
  • [26] High-level hybrid petri nets: A definition
    Giua, A
    Usai, E
    [J]. PROCEEDINGS OF THE 35TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-4, 1996, : 148 - 150
  • [27] From high-level Petri nets to SystemC
    Rust, C
    Rettberg, A
    Gossens, K
    [J]. 2003 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS, VOLS 1-5, CONFERENCE PROCEEDINGS, 2003, : 1032 - 1038
  • [28] Modelling mobility in high-level Petri nets
    Devillers, Raymond
    Klaudel, Hanna
    Koutny, Maciej
    [J]. SEVENTH INTERNATIONAL CONFERENCE ON APPLICATION OF CONCURRENCY TO SYSTEM DESIGN, PROCEEDINGS, 2007, : 110 - +
  • [29] REACHABILITY TREES FOR HIGH-LEVEL PETRI NETS
    HUBER, P
    JENSEN, AM
    JEPSEN, LO
    JENSEN, K
    [J]. THEORETICAL COMPUTER SCIENCE, 1986, 45 (03) : 261 - 292
  • [30] A class of high-level Petri Nets: XML algebraic nets
    Tang, Da
    Li, Ye
    Wang, Xiu-Kun
    [J]. Dalian Ligong Daxue Xuebao/Journal of Dalian University of Technology, 2008, 48 (06): : 912 - 918
12345