Debugging PVS specifications of control logics via event-driven simulation