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 条
  • [31] VERIFICATION OF SQUARE COMMUNICATION GRID PROTOCOLS VIA INFINITE PETRI NETS
    Shmeleva, T. R.
    Zaitsev, D. A.
    Zaitsev, I. D.
    [J]. MESM 2009: 10TH MIDDLE EASTERN SIMULATION MULTICONFERENCE, 2009, : 53 - 59
  • [32] QUALITATIVE MODEL-BASED VERIFICATION OF OPERATING PROCEDURES BY HIGH-LEVEL PETRI NETS
    GERZSON, M
    CSAKI, Z
    HANGOS, KM
    [J]. COMPUTERS & CHEMICAL ENGINEERING, 1994, 18 : S565 - S569
  • [33] Modelling data transformation processes using high-level Petri nets
    Peng, Li
    [J]. ICEIS 2007: PROCEEDINGS OF THE NINTH INTERNATIONAL CONFERENCE ON ENTERPRISE INFORMATION SYSTEMS: INFORMATION SYSTEMS ANALYSIS AND SPECIFICATION, 2007, : 533 - 536
  • [34] SPECIFICATION AND VERIFICATION OF CACHE COHERENCE PROTOCOLS USING PETRI NETS
    AHMAD, I
    SALEH, K
    [J]. INTERNATIONAL JOURNAL OF ELECTRONICS, 1995, 78 (05) : 841 - 854
  • [35] ESTIM - AN INTEGRATED ENVIRONMENT FOR THE SIMULATION AND VERIFICATION OF OSI PROTOCOLS SPECIFIED IN ESTELLE
    COURTIAT, JP
    DESAQUISANNES, P
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1992, 25 (01): : 83 - 98
  • [36] Comparative study and categorization of high-level petri nets
    Gerogiannis, VC
    Kameas, AD
    Pintelas, PE
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 1998, 43 (02) : 133 - 160
  • [37] TOWARDS REACHABILITY TREES FOR HIGH-LEVEL PETRI NETS
    HUBER, P
    JENSEN, AM
    JEPSEN, LO
    JENSEN, K
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 188 : 215 - 223
  • [38] Weak and strong composition of high-level Petri nets
    Best, E
    Lavrov, A
    [J]. CONCUR'99: CONCURRENCY THEORY, 1999, 1664 : 194 - 209
  • [39] Development of an international standard for high-level Petri nets
    Billington, J
    [J]. THIRD IEEE INTERNATIONAL SOFTWARE ENGINEERING STANDARDS SYMPOSIUM AND FORUM (ISESS 97) - EMERGING INTERNATIONAL STANDARDS, PROCEEDINGS, 1997, : 155 - 162
  • [40] Application of Petri nets in verification of distributed systems represented in the Estelle language
    Alekseev, AG
    Bystrov, AV
    Kurtov, SA
    Myl'nikov, SP
    Nepomnyashchy, VA
    Okunishnikova, EV
    Chubarev, PA
    Churina, TG
    [J]. JOURNAL OF COMPUTER AND SYSTEMS SCIENCES INTERNATIONAL, 1999, 38 (05) : 771 - 781
12345