Humboldt-Universität zu Berlin, Institut für Informatik,
Lehrstuhl für Automaten und Systemtheorie, Prof. Starke


Petri Net Tools: INA et al.


INA: Integrated Net Analyzer

INA is a tool package supporting the analysis of Place/Transition (Petri Nets) and Coloured Petri Nets.

The official Web site is: www.informatik.hu-berlin.de/lehrstuehle/automaten/ina/


inatcl and TkINA: (graphical) user interfaces

INA is not directly usable as a computing engine for other applications (it is not possible to invoke algorithms from outside the program) and does not provide a graphical user interface. Therefore inatcl and TkINA were developed.

inatcl is a tcl-based interface to (some) functionality provided by INA. It allows to write simple applications using the interpreted scripting language tcl.

As an example a script for testing the (non-)reachability of a (partial) marking using place invariants, the state equation, and (if needed) a part of the reachability graph is shown below:

#!/usr/local/bin/inatcl
set net  "dinner.pnt"
set mark "0 0 0 0 0 1 1 - 1 1 - - - - - - - 1 - -"

proc TestResult { result } {
    if { [string match "*NotReachable" $result] } {
        puts "marking is not reachable"
        ina delete
        exit
    } elseif { [string match "*Reachable" $result] } {
        puts "marking is reachable"
        ina delete
        exit
    } else {
        puts "reachability unknown"
    }
}

makeInaObject -name ina
ina readNet $net
ina check
puts "testing invariant property:"
TestResult [ina invTest mark]
puts "testing state equation:" 
TestResult [ina stateEquation mark]
puts "testing reachability:" 
TestResult [ina reachTest mark]

inatcl has some advantages for tool developers: it can be used as a computing engine working in the background of other applications. One such application is TkINA.

TkINA provides a graphical interface for starting analysis algorithms; some results are displayed in a textual format:

TkINA

TkINA is integrated in the PEP tool (Programming Envorionment based on Petri Nets) and does not provide its own graphical editor. Within the PEP tool it can be used to generate and highlight e.g. invariants, deadlocks, and state machine components.

Nevertheless TkINA can also be used as a standalone tool. Currently TkINA and inatcl are only available for systems running Sun-Solaris or Linux.

Download inatcl and TkINA version 2.2 final - Juli 31, 2003

Update TkINA in the PEP tool version 2.2 final - Juli 31, August 2003

Documentation

This work was supported by the Deutsche Forschungsgemeinschaft under the reference ``PEP''.


SESA: Signal-Net System Analyzer

SESA is the newest tool out of the INA family.

H.-M. Hanisch and M. Rausch have shown the need for a technique which is still related to Petri nets but tailored to the needs of a control engineer. The idea of condition/event systems provided by R. Sreenivas and B. Krogh guided them to a model based on Petri net representation of the dynamic behavior of basic modules of a system which has to be modeled and some extensions by incoming and outgoing signals which are used to connect the basic modules to a complete system model. A concept of one-sided synchronization of modules is provided, where a signal-event from one modul forces a simultaneous action in a second module, but only if that action is enabled. Condition-arcs are used to perform non-destructive reading of markings Since the basic model form is derived from Petri nets and the signal concept is based on condition signals and event signals, they call their models net condition/event systems (NCES). In the case of autonomous systems (these are systems with no external inputs), analysis is possible. Such autonomous systems are called signal-net systems or signal-event nets (the naming differences are due to some historical reasons).

SESA provides new and improved algorithms for the analysis of such signal-net-systems. These capabilities are used for the verification of some aspects of the execution control of function blocks following the draft standard IEC 61499 which is currently under preparatation.

Download

Papers and Documentation

Project Information

This work was supported by the Deutsche Forschungsgemeinschaft under the reference ``Funktionsblöcke''.


LoLA: Low Level Petri net Analyzer

LoLA has been implemented for the validation of reduction techniques for place/transition net reachability graphs. LoLA features symmetric as well as stubborn set based methods. Net symmetries are automatically computed. Stubborn sets are custumized to the particular analysis task. LoLA can analyse reachability of a given state, boundedness of the net or a place, dead transitions, reversibility, existence of home states. LoLA can verify formulas of a branching time logic. Addionally, there is a memory-efficient semi-decision procedure for the satisfiability of a given state predicate.

The official Web site is: www.informatik.hu-berlin.de/~kschmidt/lola.html

LoLA is developed by Karsten Schmidt kschmidt@informatik.hu-berlin.de.


Stephan Roch roch@informatik.hu-berlin.de
Juli 31, 2003