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 条
  • [1] Verification of Estelle-specified communication protocols using high-level Petri nets
    Nepomniaschy, VA
    Alekseev, GI
    Bystrov, AV
    Myl'nikov, SP
    Okunishnikova, EV
    Chubarev, PA
    Churina, TG
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2001, 27 (02) : 58 - 68
  • [2] Modeling and Verification of the SDL-Specified Communication Protocols Using High-Level Petri Nets
    Nepomniaschy, V. A.
    Argirov, V. S.
    Beloglazov, D. M.
    Bystrov, A. V.
    Chetvertakov, E. A.
    Churina, T. G.
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2008, 34 (06) : 330 - 340
  • [3] Modeling and verification of the SDL-specified communication protocols using high-level Petri nets
    V. A. Nepomniaschy
    V. S. Argirov
    D. M. Beloglazov
    A. V. Bystrov
    E. A. Chetvertakov
    T. G. Churina
    [J]. Programming and Computer Software, 2008, 34 : 330 - 340
  • [4] THE VERIFICATION OF COMMUNICATION PROTOCOLS USING NUMERICAL PETRI NETS
    SYMONS, FJW
    [J]. AUSTRALIAN TELECOMMUNICATION RESEARCH, 1980, 14 (01): : 34 - 38
  • [5] PROTEAN - A HIGH-LEVEL PETRI NET TOOL FOR THE SPECIFICATION AND VERIFICATION OF COMMUNICATION PROTOCOLS
    BILLINGTON, J
    WHEELER, GR
    WILBURHAM, MC
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1988, 14 (03) : 301 - 316
  • [6] Application of modified coloured petri nets to modeling and verification of SDL specified communication protocols
    Nepomniaschy, Valery A.
    Alekseev, Gennady I.
    Argirov, Victor S.
    Beloglazov, Dmitri M.
    Bystrov, Alexander V.
    Chetvertakov, Eugene A.
    Churina, Tatiana G.
    Mylnikov, Sergey P.
    Novikov, Ruslan M.
    [J]. COMPUTER SCIENCE - THEORY AND APPLICATIONS, 2007, 4649 : 303 - +
  • [7] Fuzzy rule base systems verification using high-level Petri nets
    Yang, SJH
    Tsai, JJP
    Chen, CC
    [J]. IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 2003, 15 (02) : 457 - 473
  • [8] Verification of distributed systems modelled by high-level Petri nets
    Kozura, VE
    Nepomniaschy, VA
    Novikov, RM
    [J]. PAR ELEC 2002: INTERNATIONAL CONFERENCE ON PARALLEL COMPUTING IN ELECTRICAL ENGINEERING, 2002, : 61 - 66
  • [9] VERIFICATION OF SPECIFICATIONS WRITTEN IN THE ESTELLE LANGUAGE USING PETRI NETS
    DIMITROV, V
    PETKOV, A
    [J]. AVTOMATIKA I VYCHISLITELNAYA TEKHNIKA, 1989, (05): : 23 - 27
  • [10] COMPOSITIONAL DESIGN AND VERIFICATION OF COMMUNICATION PROTOCOLS, USING LABELED PETRI NETS
    LLORET, JC
    AZEMA, P
    VERNADAT, F
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 531 : 96 - 105
12345