High-Level Petri Net Model Checking with AlPiNA

被引：13

作者：

Hostettler, Steve ^{[1
]}

Marechal, Alexis ^{[1
]}

Linard, Alban ^{[1
]}

Risoldi, Matteo ^{[1
]}

Buchs, Didier ^{[1
]}

机构：

[1] Univ Geneva, Ctr Univ Informat, CH-1227 Carouge, Switzerland

来源：

FUNDAMENTA INFORMATICAE | 2011年 / 113卷 / 3-4期

关键词：

System design and verification; Higher-level Nets Models; Algebraic Petri Nets; State Space Generation; Computer Tools for Nets; Model Checking; DECISION DIAGRAMS; SPECIFICATION;

D O I：

10.3233/FI-2011-608

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

Although model checking is heavily used in the hardware domain, it did not take off in software engineering yet. One of the possible reasons is that software models are very complex. They integrate many dimensions such as data types and concurrency, leading to the infamous state space explosion problem. This article introduces the Algebraic Petri Nets Analyzer (AlPiNA), a symbolic model checker for High-level Petri nets. It is comprised of two independent modules: a GUI plug-in for Eclipse and an underlying model checking engine. AlPiNA is a step towards performing efficient and user-friendly model checking of large software systems. This is achieved by separating the model and its properties from the optimisation artifacts. This article describes the features that AlPiNA provides to the user for designing models and verifying properties. It also presents the techniques and artifacts used for tuning verification performance, along with some theoretical background.

引用

页码：229 / 264

页数：36

共 50 条

[1] Application of Petri Net Model in High-Level Scheduling Algorithm
Srivastava, Atul Kumar
Tiwari, Siddharth
Banerjee, Shubhanker
[J]. ADVANCES IN VLSI, COMMUNICATION, AND SIGNAL PROCESSING, 2020, 587 : 705 - 717
[2] A generalized stochastic high-level Petri net model for performance analysis
Koriem, SM
Patnaik, LM
[J]. JOURNAL OF SYSTEMS AND SOFTWARE, 1997, 36 (03) : 247 - 265
[3] Knowledge verification with an enhanced high-level Petri-net model
Wu, CH
Lee, SJ
[J]. IEEE EXPERT-INTELLIGENT SYSTEMS & THEIR APPLICATIONS, 1997, 12 (05): : 73 - 80
[4] HIGH-LEVEL PETRI-NET MODEL OF LOGIC PROGRAM WITH NEGATION
LI, LW
[J]. IEEE TRANSACTIONS ON KNOWLEDGE AND DATA ENGINEERING, 1994, 6 (03) : 382 - 395
[5] High-Level Petri Nets with Object-Orientation - A High-Level Petri Net Model Allowing Multiple Inheritance and Multiple Polymorphism
Brezovan, Marius
Burdescu, Dumitru
Ganea, Eugen
Stanescu, Liana
[J]. INTELLIGENT DISTRIBUTED COMPUTING IV, 2010, 315 : 219 - 228
[6] ON THE ANALYSIS OF STOCHASTIC HIGH-LEVEL PETRI NET MODELS
LIN, C
MARINESCU, DC
[J]. MICROELECTRONICS AND RELIABILITY, 1991, 31 (04): : 747 - 767
[7] High-level Petri net approach for supervisory control
Zouari, B
[J]. 2003 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS, VOLS 1-5, CONFERENCE PROCEEDINGS, 2003, : 1161 - 1166
[8] Behaviour and instantiation of high-level Petri net processes
Ehrig, H
[J]. FUNDAMENTA INFORMATICAE, 2005, 65 (03) : 211 - 247
[9] HIGH-LEVEL PETRI-NET MODEL FOR A RESOURCE-SHARING PROBLEM
DATTA, AK
GHOSH, S
[J]. INFORMATION SCIENCES, 1990, 51 (02) : 213 - 220
[10] A high-level Petri net based model for web services composition and verification
Chemaa, Sofiane
Bouarioua, Mouna
Chaoui, Allaoua
[J]. INTERNATIONAL JOURNAL OF COMPUTER APPLICATIONS IN TECHNOLOGY, 2015, 51 (04) : 306 - 323

← 1 2 3 4 5 →