Mcta
Subproject |
R3 |
Categories |
Model checker for hard & soft real-time systems |
Overview |
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. Mcta accelerates the detection of error states by using the directed model checking approach. Directed model checking is a technique that is tailored to fast detection of system states that violate a given safety property. This is achieved by influencing the order in which states are explored during the state space traversal. The order is typically determined by an abstract distance function that estimates a state's distance to a nearest error state. Based on the estimated error distances, Mcta allows the user to choose between several strategies to explore the state space, including the two wide-spread search methods A* and greedy search. Mcta generates the abstract distance values fully automatically for each input given by a network of timed automata and a safety property. This is done by efficiently computing a rather coarse abstraction (the user can choose among several kinds of abstraction) and taking the distance in the abstract state space. |
S. Kupferschmid, M. Wehrle, B. Nebel, and A. Podelski. Faster than Uppaal? In Aarti Gupta and Sharad Malik, editor, Proceedings of the 20th International Conference on Computer Aided Verification (CAV 2008), volume 5123 of Lecture Notes in Computer Science (LNCS), pages 552-555, 2008. |
|
Benchmarks |
|
Download |
|
Manual |
|
Status |
Stable |