PV3 ⊧ IMITATOR: Inverse Method for Inferring Time Abstract behaviorcan perform a number of actions on a network of automata and a set of desired properties

Tool for automated parameter synthesis for concurrent timed systems

Application domain/field

• Parametric verification
• Real-time systems
• Safety analysis
• Reachability analysis
• Model checking
• Parameter synthesis
• Timed automata

Type of tool

Model checker?

Expected input

• Network of IMITATOR parametric timed automata (NIPTA)
• Property to check

Format:

Own syntax/input language (.imi file) Property should be in a separate file (.imiprop file)

Expected output

? (depends on what analysis is done with the tool)

Internals

IMITATOR implements the following algorithms:

• On-the-fly computation of the parametric state space
• Parametric reachability or safety analysis
• Minimal-time reachability synthesis
• Parametric deadlock freeness checking
• Parametric loop synthesis, and non-Zeno loop synthesis
• Robustness analysis
• Behavioral cartography algorithm
• PRP and PRPC

Uses Parma Polyhedra Library (PPL)

Comments

License: GPL v3