DESpot includes tools to work with timed and untimed flat DES projects in order to verify properties for fault-tolerant supervisory control. In particular it include tools to verify fault-tolerant timed and untimed controllability and nonblocking properties, for several fault scenarios.
This help section explains how to specify the necessary parameters for these tools, as well as how to run these tools.
For more information on fault-tolerant supervisory control, please refer to:
Aos Mulahuwaish, "Fault-Tolerant Supervisory Control," Phd Thesis, Dept. of Computing and Software, McMaster University, May. 2019.
Amal Alsuwaidan, "Timed Fault Tolerant Supervisory Control," M.A.Sc. Thesis, Dept. of Computing and Software, McMaster University, April 2016.