Logik und Formale Methoden

MOCHA

Classical black-box conformance testing is becoming the bottleneck in many system development projects because the number of required test cases explodes. MOCHA aims at tackling this problem by designing a new method for automated test generation (ATG) using model checking. This will be achieved by developing a tool-independent theoretical foundation and by uniting the two existing approaches of on-the-fly and off-the-fly ATG into lazy on-the-fly ATG.

As the main progress over existing technology, lazy on-the-fly ATG efficiently produces more revealing tests and supports reproducible testing for nondeterministic systems.