UNIGE document Scientific Article
previous document  unige:18361  next document
add to browser collection
Title

High-Level Petri Net Model Checking with AlPiNA

Authors
Published in Fundamenta Informaticae. 2011, vol. 113, no. 3-4, p. 229-264
Abstract 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 net. 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.
Keywords System design and verificationHigher-level Nets ModelsAlgebraic Petri NetsState Space GenerationComputer Tools for NetsModel Checking
Identifiers
Full text
Article (Author postprint) (1.2 MB) - public document Free access
Structures
Research group Software Modeling and Verification
Citation
(ISO format)
HOSTETTLER, Steve Patrick et al. High-Level Petri Net Model Checking with AlPiNA. In: Fundamenta Informaticae, 2011, vol. 113, n° 3-4, p. 229-264. https://archive-ouverte.unige.ch/unige:18361

383 hits

405 downloads

Update

Deposited on : 2012-02-09

Export document
Format :
Citation style :