parameter synthesis

Guaranteeing Timed Opacity using Parametric Timed Model Checking

Among harmful information leaks, the timing information leakage occurs whenever an attacker successfully deduces confidential internal information depending on the system execution time. We address the following timed opacity problem: given a timed system, a private location and a final location, synthesize the execution times from the initial location to the final location for which one cannot deduce whether the system went through the private location.