The Pr/T-net reachability analysis tool PROD implements several methods for efficient reachability analysis.
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:
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.
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.
kolumbus.fi>