High-Level Petri Net Model Checking with AlPiNA
Copyright policy )High-Level Petri Net Model Checking with AlPiNA
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.
- University of Geneva Switzerland
system design, algebraic Petri nets, Specification and verification (program logics, model checking, etc.), State Space Generation, Distributed systems, higher-level net models, state space generation, Model Checking, Theoretical Computer Science, System design and verification, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), 025.063, Higher-level Nets Models, unfolding, Algebra and Number Theory, Computer Tools for Nets, Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.), decision diagrams, topological and algebraic clustering, model checking, Computational Theory and Mathematics, Algebraic Petri Nets, verification, Information Systems
system design, algebraic Petri nets, Specification and verification (program logics, model checking, etc.), State Space Generation, Distributed systems, higher-level net models, state space generation, Model Checking, Theoretical Computer Science, System design and verification, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), 025.063, Higher-level Nets Models, unfolding, Algebra and Number Theory, Computer Tools for Nets, Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.), decision diagrams, topological and algebraic clustering, model checking, Computational Theory and Mathematics, Algebraic Petri Nets, verification, Information Systems
selected citations These citations are derived from selected sources.This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).15 popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network.Average influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically).Top 10% impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network.Top 10%
Citations provided by BIP!Popularity provided by BIP!