Runtime Verification

( ) Знакомство с интерфейсом replay <-> ProB и его реализацией в java-библиотеках
( ) Нулевая версия: все параметры всех событий есть в модельной трассе
( ) Отладка нулевой версии
( ) Первая версия: недостающие параметры событий вычисляются, поддерживаются некоторые шаблоны охранных условий
( ) Отладка первой версии
( ) Вторая версия: исследование потенциальных охранных условий, из которых можно эффективно автоматически восстанавливать отсутствующие параметры
( ) Отладка второй версии