TChecker is an open source library and tool for model-checking timed automata. This webpage offers an online demo of TChecker that can be used to test the tools on small models.
Please visit the GitHub repository https://github.com/ticktac-project/tchecker to access the source code.
Installation instructions as well as the documentation of tools and tutorials are available from the wiki page.
Please, also consider our companion tool uppaal-to-tchecker that translates UPPAAL models into TChecker models.
TChecker file format is described on this page.