Verification of distributed systems modelled by high-level Petri nets

被引:9
|
作者
Kozura, VE [1 ]
Nepomniaschy, VA [1 ]
Novikov, RM [1 ]
机构
[1] Russian Acad Sci, Inst Informat Syst, Sibirian Div, Novosibirsk 630090, Russia
关键词
D O I
10.1109/PCEE.2002.1115202
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
A tool PNV (Petri net verifier) designed for analysis, modelling and verification of coloured Petri nets (CPN) is presented in the paper. The tool consists of two main components: a translator which generates an internal form of CPN and a C++ program modelling the input CPN, and a model-checking component which is applied to CPN limited by finite state systems when properties are presented in mu-calculus. Moreover, the translator generates a program in Pascal extended by a nondeterministic construct in order to model and verify the input CPN. The model-checking component uses the internal form of CPN and includes a model constructor which generates the reachability graph of CPN, and a model-checker The paper describes a model-checking experiment with CPN which model the ring communication protocol [7]. An ineffectiveness of the ring protocol is proven by the experiment, and a modified effective ring protocol is verified too.
引用
收藏
页码:61 / 66
页数:6
相关论文
共 50 条
  • [1] 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
  • [2] Rapid prototyping of parallel and distributed systems by means of high-level Petri nets
    Mikolajczak, B
    Cabeza, A
    Rumbut, JT
    [J]. SMC '97 CONFERENCE PROCEEDINGS - 1997 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: CONFERENCE THEME: COMPUTATIONAL CYBERNETICS AND SIMULATION, 1997, : 1735 - 1740
  • [3] FORMALIZING DISTRIBUTED SELF-ADAPTIVE SYSTEMS USING HIGH-LEVEL PETRI NETS
    Capra, Lorenzo
    Camilli, Matteo
    [J]. PROCEEDINGS OF THE 2019 SUMMER SIMULATION CONFERENCE (SUMMERSIM '19), 2019,
  • [4] Design of parallel and distributed systems with high-level Petri nets using case technology
    Mikolajczak, B
    Rumbut, JT
    [J]. INFORMATION INTELLIGENCE AND SYSTEMS, VOLS 1-4, 1996, : 2288 - 2293
  • [5] Augmenting High-Level Petri Nets to Support GALS Distributed Embedded Systems Specification
    Moutinho, Filipe
    Gomes, Luis
    [J]. TECHNOLOGICAL INNOVATION FOR THE INTERNET OF THINGS, 2013, 394 : 221 - 228
  • [6] Rapid prototyping of distributed computing systems using high-level Petri nets with objects
    Mikolajczak, B
    [J]. PROCEEDINGS OF THE HIGH-PERFORMANCE COMPUTING (HPC'98), 1998, : 388 - 393
  • [7] HIGH-LEVEL ALGEBRAIC PETRI NETS
    KAN, CY
    HE, XD
    [J]. INFORMATION AND SOFTWARE TECHNOLOGY, 1995, 37 (01) : 23 - 30
  • [8] Z AND HIGH-LEVEL PETRI NETS
    VANHEE, KM
    SOMERS, LJ
    VOORHOEVE, M
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1991, 551 : 204 - 219
  • [9] Object-Based High-Level Petri Nets as a formal approach to distributed information systems
    Guerrero, DDS
    deFigueiredo, JCA
    Perkusich, A
    [J]. SMC '97 CONFERENCE PROCEEDINGS - 1997 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN, AND CYBERNETICS, VOLS 1-5: CONFERENCE THEME: COMPUTATIONAL CYBERNETICS AND SIMULATION, 1997, : 3383 - 3388
  • [10] Design of intelligent mechatronical systems with high-level Petri nets
    Koch, M
    Rust, C
    Kleinjohann, B
    [J]. PROCEEDINGS OF THE 2003 IEEE/ASME INTERNATIONAL CONFERENCE ON ADVANCED INTELLIGENT MECHATRONICS (AIM 2003), VOLS 1 AND 2, 2003, : 217 - 222