2

Guaranteeing timed opacity using parametric timed model checking