Tina

Overview

Entry last updated: 2005/4/26
Entry last validated: 2005/4/26

Tool homepage: http://www.laas.fr/tina

Tool availability: Free of charge

Tool Features

Petri Nets Supported (see also help on terminology)

Place/Transition Nets
Petri Nets with Time
Time Petri Nets

Components (see also help on terminology)

Graphical Editor
Token Game Animation
State Spaces
Condensed State Spaces
Place Invariants
Transition Invariants
State Class Spaces

Environments

Sun, SunOS
PC, Linux
PC, MS Windows 98
PC, MS Windows NT
PC, MS Windows 2000
PC, MS Windows XP
Macintosh, Mac OS X

Tool Description

Tina is a toolbox for analysis of Petri nets and Time Petri nets. At that time, it includes:

nd: An editor for Petri nets, Time Petri nets, and automata, in textual or graphical form, interfaced with drawing tools and the analysis tools below. A stepper/simulator operating both in graphical and textual modes is packed with the editor.

tina: Builds various reachability graphs or state space abstractions for Petri nets and Time Petri nets. For Petri Nets: coverability graphs, markings graphs, and various partial graphs using Covering steps, Stubborn or Persistent sets, or Persistent steps. For Time Petri nets: various state class graph constructions, preserving markings, states, linear time properties, or branching time properties. Results may be produced in several popular formats.

struct: Computes semiflows (invariants) or flows on places and/or transitions, with various options.

Contact Information

LAAS-CNRS
7, avenue du Colonel Roche
31077 Toulouse CEDEX
France

Phone:  +33/(0)5 61 33 63 63
Fax:    +33/(0)5 61 33 64 11
E-mail: Bernard.Berthomieu@laas.fr

Other Remarks

Modelcheckers for LTL and the mu-calculus are forthcoming. No direct support is currently provided for performance or timeliness analysis, but many of such requirements can be checked by composing the Time Petri net models with "observer" nets that assert or contradict the properties to be proven.

The maintainers of this page