You are here: Home Tools MCTA

MCTA

Mcta is a model checking tool for real-time specifications modelled as timed automata. Although the tool can be used for verification, Mcta is rather optimized for falsification, i.e., detecting violations against safety properties fast and returning short error traces. Several types of traces can be generated, including an option to find a (guaranteed) shortest error trace. For more information, please contact Martin Wehrle.