Guaranteeing timed opacity using parametric timed model checking