What is 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. There is also the possibility to examine Mcta's traces with Uppaal's graphical user interface.
Mcta accepts input models in the form of the Uppaal input language (cf. [1]). So far only a fraction thereof is supported e.g., there is no support for urgent channels, arrays, etc. yet. Internally, Mcta uses Uppaal's timed automata parser library. For the representation of zones Mcta uses Uppaal's difference bound matrices library. Both libraries are released under the terms of the LGPL or GPL, respectively, and are freely available from here. All other data structures and all algorithms (and their implementation) used are genuine to Mcta.
Mcta accelerates the detection of error states with directed model checking. In this approach, the traversal of the state space is guided by a heuristic function which estimates the distance of a search state to the nearest error state. The search then gives preference to states with lower value. Read more.
Mcta is free software and also released under the terms of the GPL. Pre-compiled Linux executables and a snapshot of the source code of our tool are also freely available in the download section.
In the literature section you can find papers describing Mcta, the implemented techniques and the benchmarks.
Mcta is mainly developed by Sebastian Kupferschmid and Martin Wehrle within the AVACS project (Automatic Verification and Analysis of Complex Systems).
