Посмотрите на Спина и Промелу. Spin - это средство проверки моделей, которое проходит через все состояния, в которых может находиться ваш код, для поиска потерь в безопасности и жизнеспособности. Как вы хотите, с помощью spin вы можете пройти через него самостоятельно и выбрать, какая опция будет запущена следующей и какие значения должны иметь вещи. Вам нужно написать раздел, который вы хотите протестировать, в коде Promela, который похож на c. Spin лучше, чем обычные средства отладки - многопоточные программы не работают каждый раз одинаково, поэтому средство проверки моделей более полезно, чем стандартный отладчик.