Selected publications at LSV

Abstract:
We present here the user manual of IMITATOR II, a tool implementing the "inverse method" in the framework of parametric timed automata: given a reference valuation of the parameters, its generates a constraint such that the system behaves the same as under the reference valuation in terms of traces, i.e., alternating sequences of locations and actions. This is useful for safely relaxing some values of the reference valuation, and optimizing timing bounds of the system.
    Besides the inverse method, IMITATOR II also implements the "behavioral cartography algorithm", allowing to solve the following good parameters problem: find a set of valuations within a given rectangle for which the system behaves well.
    We give here the installation requirements and the launching commands of IMITATOR II, as well as the source code of a toy example.

@techreport{rr-lsv-10-20,
   author = {Andr{\'e}, {\'E}tienne},
   institution = {Laboratoire Sp{\'e}cification et V{\'e}rification, ENS Cachan, France},
   month = nov,
   note = {31~pages},
   number = {LSV-10-20},
   type = {Research Report},
   title = {{IMITATOR}~{II} User Manual},
   url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PDF/ rr-lsv-2010-20.pdf},
   year = {2010},
}