Selected publications at LSV

Given a Parametric Timed Automaton (PTA) A and a tuple π0 of reference valuations for timings, the Inverse Method (IM) synthesizes a constraint around π0 where A behaves in the same time-abstract manner. This provides us with a quantitative measure of robustness of the behavior of A around π0. We show in this paper how IM can be applied in a specific way to treat the robustness of scheduling systems. We also explain how to use the method in order to synthesize large zones of the timing parameter space where the system is guaranteed to be schedulable. We illustrate the method on several examples of the literature as well as a case study originating from an industrial design project.

   address = {Leicester, UK},
   author = {Fribourg, Laurent and Lesens, David and Moro, Pierre and Soulat, Romain},
   booktitle = {{P}roceedings of the 19th {I}nternational {S}ymposium on {T}emporal {R}epresentation and {R}easoning ({TIME}'12)},
   DOI = {10.1109/TIME.2012.10},
   editor = {Reynolds, Mark and Terenziani, Paolo and Moszkowski, Ben},
   month = sep,
   pages = {73-80},
   publisher = {{IEEE} Computer Society Press},
   title = {Robustness Analysis for Scheduling Problems using the Inverse Method},
   url = {},
   year = {2012},

About LSV