Tool homepage: http://www.tcs.hut.fi/Software/prod/
Tool availability: Free of charge
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.
Kimmo Varpaaniemi Koivukyl„n puistotie 14 A 5 FI-01360 Vantaa Finland Phone: +358 9 871 4976 Fax: E-mail: kimmo.varpaaniemi@kolumbus.fi
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.