Verification of protocol ECMA with decomposition of Petri net model

被引：0
|
作者：
Zaitsev, DA [1 ]
机构：
[1] Odessa Natl Telecommun Acad, UA-62029 Odessa, Ukraine
来源：
ISAS/CITSA 2004: International Conference on Cybernetics and Information Technologies, Systems and Applications and 10th International Conference on Information Systems Analysis and Synthesis, Vol 3, Proceedings | 2004年
关键词：
protocol; Petri net; invariant; functional subnet; decomposition;
D O I：
暂无
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
Decomposition of Petri net model of ECMA communication protocol into minimal functional subnets, left and right communicating systems, subsystems of connection establishing and disconnecting is implemented. A correct protocol ought to be invariant one. Invariance of source model is proved on the base of established invariance of functional subnets. Isomorphism of subnets has allowed the calculation of invariants in the process of consecutive composition of net. Acceleration of computations for decomposition technique was estimated. It is exponential with the respect to net dimension.
引用
收藏
页码：231 / 236
页数：6
相关论文
共 50 条
  • [1] Petri Net Model of Session Initiation Protocol and Its Verification
    Yang Peng
    Yuan Zhanting
    Wang Jizeng
    [J]. 2007 INTERNATIONAL CONFERENCE ON WIRELESS COMMUNICATIONS, NETWORKING AND MOBILE COMPUTING, VOLS 1-15, 2007, : 1861 - +
  • [2] A coloured Petri net approach to protocol verification
    Billington, J
    Gallasch, GE
    Han, B
    [J]. LECTURES ON CONCURRENCY AND PETRI NETS: ADVANCES IN PETRI NETS, 2004, 3098 : 210 - 290
  • [3] PROTOCOL VERIFICATION TOOL WITH EXTENDED PETRI-NET AND HORN CLAUSE
    WATANABE, T
    OHTA, T
    SATO, F
    MIZUNO, T
    [J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 1995, E78A (11) : 1458 - 1467
  • [4] System simulation and verification method based on Petri net model
    Ke W.
    Chen J.
    Jiang S.
    [J]. 1600, Chinese Institute of Electronics (39): : 924 - 930
  • [5] A Method for Soundness Verification of Workflow Model Based on Petri Net
    Wang Jianliang
    Xia Zhiwei
    Ding Yanan
    [J]. ICCSSE 2009: PROCEEDINGS OF 2009 4TH INTERNATIONAL CONFERENCE ON COMPUTER SCIENCE & EDUCATION, 2009, : 880 - 883
  • [6] Verification of batch plant using timed Petri net model
    Li, HG
    Swani, AH
    [J]. System Simulation and Scientific Computing, Vols 1 and 2, Proceedings, 2005, : 861 - 865
  • [7] Petri net based Verification of a Cooperative Work flow Model
    Annappa, B.
    Jiju, P.
    Chandrasekaran, K.
    Shet, K. C.
    [J]. NDT: 2009 FIRST INTERNATIONAL CONFERENCE ON NETWORKED DIGITAL TECHNOLOGIES, 2009, : 82 - 87
  • [8] Petri net-based verification of security protocol implementation in software evolution
    Bin Ahmadon, Mohd Anuaruddin
    Yamaguchi, Shingo
    Gupta, B. B.
    [J]. INTERNATIONAL JOURNAL OF EMBEDDED SYSTEMS, 2018, 10 (06) : 503 - 517
  • [9] Timed Colored Petri Net (CPN) model of the Session Initiation Protocol (SIP) for formal verification of mobile applications
    Yim, Jaegeol
    Lee, Gyeyoung
    Shim, Kyubark
    [J]. ASIA LIFE SCIENCES, 2015, : 415 - 426
  • [10] Diagnosability verification with Petri net unfoldings
    Madalinski, Agnes
    Nouioua, Farid
    Dague, Philippe
    [J]. INTERNATIONAL JOURNAL OF KNOWLEDGE-BASED AND INTELLIGENT ENGINEERING SYSTEMS, 2010, 14 (02) : 49 - 55
12345