Searching for just a few words should be enough to get started. If you need to make more complex queries, use the tips below to guide you.
Issue title: Applications and Theory of Petri Nets and Other Models of Concurrency, 2010
Article type: Research Article
Authors: Hostettler, Steve | Marechal, Alexis | Linard, Alban | Risoldi, Matteo | Buchs, Didier
Affiliations: Centre Universitaire d'Informatique, Université de Genève, Route de Drize 7, CH-1227 Carouge, Switzerland. steve.hostettler@unige.ch; alexis.marechal@unige.ch; alban.linard@unige.ch; matteo.risoldi@unige.ch; didier.buchs@unige.ch;
Note: [] This work was partially supported by the COMEDIA project funded by the Hasler foundation, project #2107. Address for correspondence: Route de Drize 7, CH-1227 Carouge, Switzerland
Note: [] This work was partially supported by the COMEDIA project funded by the Hasler foundation, project #2107.
Note: [] This work was partially supported by the BRINTA project funded by the Fonds National Suisse de la Recherche Scientifique, #200021-130159.
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 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.
Keywords: System design and verification, Higher-level Nets Models, Algebraic Petri Nets, State Space Generation, Computer Tools for Nets, Model Checking
DOI: 10.3233/FI-2011-608
Journal: Fundamenta Informaticae, vol. 113, no. 3-4, pp. 229-264, 2011
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
USA
Tel: +1 703 830 6300
Fax: +1 703 830 2300
sales@iospress.com
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
IOS Press
Nieuwe Hemweg 6B
1013 BG Amsterdam
The Netherlands
Tel: +31 20 688 3355
Fax: +31 20 687 0091
info@iospress.nl
For editorial issues, permissions, book requests, submissions and proceedings, contact the Amsterdam office info@iospress.nl
Inspirees International (China Office)
Ciyunsi Beili 207(CapitaLand), Bld 1, 7-901
100025, Beijing
China
Free service line: 400 661 8717
Fax: +86 10 8446 7947
china@iospress.cn
For editorial issues, like the status of your submitted paper or proposals, write to editorial@iospress.nl
如果您在出版方面需要帮助或有任何建, 件至: editorial@iospress.nl