Real-time systems can be used in a wide range of applications, such as transport, telecommunications and industry. However, accidents can happen, and it is necessary to have confidence in these systems in order to avoid them. It is therefore necessary to formally prove that their behavior will comply with a specification. This specification can be of two kinds: with safety properties, showing that the system will always behave as expected, and security properties, showing that it will be resistant to certain attacks. For this, the formalism of timed automata (TAs) is fairly common.