Dylan Marinho

IMITATOR is a software tool for parametric verification and robustness analysis of real-time systems with parameters. It relies on the formalism of networks of parametric timed automata, augmented with rational-valued global variables, stopwatches, multi-rate clocks, and some other useful features.

strategFTO is an open source software tool to perform the exhibition of a controller for opacity, ie a set of controllable actions, such that the system is fully timed-opaque. It iteratively constructs strategies and check full timed opacity.