High-Level Petri Net Model Checking with AlPiNA
| Autor: | Steve Hostettler, Alban Linard, Didier Buchs, Alexis Marechal, Matteo Risoldi |
|---|---|
| Rok vydání: | 2011 |
| Předmět: |
Model checking
Computer science Concurrency 0102 computer and information sciences 02 engineering and technology State Space Generation computer.software_genre 01 natural sciences Model Checking Theoretical Computer Science Domain (software engineering) Software System design and verification 0202 electrical engineering electronic engineering information engineering Higher-level Nets Models Software system ddc:025.063 Algebra and Number Theory Computer Tools for Nets business.industry Programming language Abstraction model checking Petri net Process architecture Computational Theory and Mathematics 010201 computation theory & mathematics Algebraic Petri Nets 020201 artificial intelligence & image processing business computer Information Systems |
| Zdroj: | Fundamenta Informaticae, Vol. 113, No 3-4 (2011) pp. 229-264 FUNDAMENTA INFORMATICAE |
| ISSN: | 0169-2968 |
| DOI: | 10.3233/fi-2011-608 |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|