On the Contribution of a τ-simulation in the Incremental Modeling of Timed Systems

We are interested in the preservation of linear-time properties during incremental modeling of timed systems. We consider timed systems modeled by timed automata in a compositional framework. Their requirements are expressed by the logical formalism MITL (Metric Interval Temporal Logic).We propose to use τ-simulations as a way to preserve such properties during an incremental modeling, i.e., either integration of components or refinement. We define τ-simulation relations on the semantics of timed automata in order to handle the preservation of liveness properties. Moreover, we implemented a tool to verify such τ-simulations, based on Open-Kronos libraries and using the tool Profounder.