[FEATURE] #12321
openГенерацию тестов для ядра операционной системы по непокрытым состояниям модели
0%
Description
( ) Генерацию тестов для ядра операционной системы по непокрытым состояниям модели (~6 месяцев)
( ) генерация самых простых случаев (месяц)
( ) Пересборка ProB (если понадобиться лезть внутрь) (8 рабочих дней)
( ) Реконструция цепочек системных вызовов и начального окружения для достижения непокрытых состояний (6 месяцев)
Updated by Denis Efremov about 1 year ago
В ProB есть поддержка генерации тестов, два режима: model-checking-based, constraint-based. https://www3.hhu.de/stups/handbook/prob2/prob_handbook.html#test-case-generation Нужно попробовать, насколько это работает с нашей моделью. Две проблемы: 1 - как сформулировать критерий для покрытия, позволяющий выдать инструменту что-нибудь адекватное, 2 - синхронизация начальных состояний, как и в случае с прогоном трасс на модели. В прогоне тестов мы сейчас используем очень простой способ для синхронизации: сам тест состоит из одного, максимум двух системных вызовов. Подготовка начального окружения производится до теста, при воспроизведении оно конструируется медиатором. Предлагаю и здесь начинать с этого же: подготовить состояние модели с заданными данными (наполнить множества начальными данными), сформулировать простой критерий, чтобы генерировались один-два события по модели.
Взять данные для модели можно с одной из трасс, например, здесь https://forge.ispras.ru/attachments/7516 до switch_mode(TRUE) или login. Либо запросить у меня в другом виде, если с такими данными ProB работать не будет. Из описания генерации тестов не очень понятно, можно ли там сначала "предварительно" выполнить несколько событий или он всегда пробует строить тест от начального состония. Если второе, то можно попытаться динамически менять INITIALIZE с нашими данными.