Modeling and verification of the SDL-specified communication protocols using high-level Petri nets

被引：0
|
作者：
V. A. Nepomniaschy
V. S. Argirov
D. M. Beloglazov
A. V. Bystrov
E. A. Chetvertakov
T. G. Churina
机构：
[1] Russian Academy of Sciences,Ershov Institute of Information Systems, Siberian Branch
[2] Novosibirsk State University,undefined
来源：
Programming and Computer Software | 2008年 / 34卷
关键词：
Process Instance; Input Place; Service Place; Output Place; Model Check Method;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
To simplify modeling and verification of communication protocols presented in the SDL language, the so-called hierarchical typed timed Petri nets (HTT nets), which are substantial modifications of colored Petri nets, are introduced. A method of translation of the SDL language into HTT nets is described. A program complex SPV (SDL Protocol Verifier), which includes a translator from SDL into HTT nets and means for editing, simulation, visualization, and verification of these net models, is presented. For the verification, a model checking method for properties presented by μ-calculus formulas is used. Experiments on application of the SPV complex for modeling and verifying two ring protocols (RE and ATMR protocols), an optimized version of the sliding window protocol (i-protocol), and a dynamic version of the InRes protocol are described
引用
收藏
页码：330 / 340
页数：10
相关论文
共 50 条
  • [1] 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
  • [2] 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
  • [3] Verification of Estelle-Specified Communication Protocols Using High-Level Petri Nets
    V. A. Nepomniaschy
    G. I. Alekseev
    A. V. Bystrov
    S. P. Myl'nikov
    E. V. Okunishnikova
    P. A. Chubarev
    T. G. Churina
    [J]. Programming and Computer Software, 2001, 27 : 58 - 68
  • [4] 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 - +
  • [5] THE VERIFICATION OF COMMUNICATION PROTOCOLS USING NUMERICAL PETRI NETS
    SYMONS, FJW
    [J]. AUSTRALIAN TELECOMMUNICATION RESEARCH, 1980, 14 (01): : 34 - 38
  • [6] MODELING OF COMMUNICATION PROTOCOLS BY USING PETRI NETS
    ILYAS, M
    KHALIL, H
    [J]. COMPUTERS & INDUSTRIAL ENGINEERING, 1986, 11 (1-4) : 547 - 551
  • [7] Modeling Multicasting in Communication Spaces by Reconfigurable High-level Petri Nets
    Ermel, Claudia
    Modica, Tony
    Biermann, Enrico
    Ehrig, Hartmut
    Hoffmann, Kathrin
    [J]. 2009 IEEE SYMPOSIUM ON VISUAL LANGUAGES AND HUMAN-CENTRIC COMPUTING, PROCEEDINGS, 2009, : 47 - 50
  • [8] 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
  • [9] SYSTEM MODELING WITH HIGH-LEVEL PETRI NETS
    GENRICH, HJ
    LAUTENBACH, K
    [J]. THEORETICAL COMPUTER SCIENCE, 1981, 13 (01) : 109 - 136
  • [10] 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
12345