AlPiNA

Overview

Entry last updated: 2010/3/5
Entry last validated: 2010/3/5

Tool homepage: http://alpina.unige.ch/

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

High-level Petri Nets

Components (see also help on terminology)

Graphical Editor
State Spaces
Condensed State Spaces
Simple Performance Analysis
Interchange File Format

Environments

Java

Tool Description

AlPiNA is a graphical editor and model checker for a class of high-level Petri nets called Algebraic Petri Nets. Its main purpose is to perform reachability checks on complex models.

AlPiNA is implemented as an Eclipse plugin. The user interface was created using the EMP metamodeling approach. Thus, models are easy to implement, without the need to know the underlying techniques related to model checking performance.

The actual model checking is performed in an independent engine, implemented in Java. It performs symbolic model checking based on ΣDD, an eﬃcient evolution in the Decision Diagrams ﬁeld, using novel techniques such as algebraic clustering and algebraic unfolding. This allows to check models with very large state spaces.

Contact Information

Prof. Didier Buchs
Computer Science Department
University of Geneva
7 route de Drize, BＵ. A, 
CH-1227 Carouge 
Switzerland

Phone:  0041 22 37 90 161
Fax:    0041 22 37 90 250
E-mail: didier.buchs@unige.ch

Other Remarks

This program is free software, it can be redistributed and/or modified under the terms of the GNU General Public License.

The maintainers of this page