PROD

Overview

Tool homepage: http://www.tcs.hut.fi/Software/prod/

Tool availability: Free of charge

Tool Features

• High-level Petri Nets
• Place/Transition Nets

• State Spaces
• Condensed State Spaces
• LTL Model Checking, CTL Model Checking

Environments

• Sun, SunOS
• HP, HP-UX
• Silicon Graphics, IRIX
• PC, Linux
• PC, MS Windows 95
• PC, MS Windows 98
• PC, MS Windows NT
• PC, MS Windows 2000
• PC, MS Windows XP

Tool Description

PROD is a text-based tool that can be used in UNIX (any system of that kind) and in Windows (3.1, 3.11, '95, NT, '98, 2000, XP). Currently no graphical user-interface exists. PROD supports the following reduced reachability graph generation methods that may also be combined:

• The stubborn set method.
• The sleep set method.
• Priority definitions.
• The use of symmetries.

PROD supports verification of CTL formulas from the reachability graph, and on-the-fly verification of LTL formulas using e.g. the stubborn set method.

Contact Information

Kimmo Varpaaniemi

Koivukyl„n puistotie 14 A 5
FI-01360 Vantaa
Finland

Phone:  +358 9 871 4976
Fax:    
E-mail: kimmo.varpaaniemi@kolumbus.fi

Other Remarks

PROD has been used e.g. in the Emma project and in the analysis of the Frame Synchronised Ring, a video on demand system, an authentication protocol (HUT-TCS Reports A29, A36, B14), the ISDN-DSS1 protocol, and a PLC-based railway traffic control system.

Documentation for PROD is available as HUT-TCS Report B13 with an up-to-date addendum. Those who download the tool get this documentation automatically.