WCET-Aware Reachability for Verified Simplex Design