Результаты верификации
Четвёртый шаг состоит в проведении верификации, которая проводилась следующим образом: каждый из автоматов, записанный текстом в некотором формате, автоматически преобразовывался в формат Stater.Далее при помощи Staterдля каждого авотмата была построена Spin-модель и выполнена верификация.
По результатам верификации оказалось, что из 800 автоматов только 231 удовлетворяет спецификации. Таким образом, для 231 программы удалось доказать корректность работы. Вопрос о корректности остальных автоматов
остается открытым. Возможно, для доказательства их корректности требуется строить другие гипотезы.
Выводы по главе 5
Предложен подход к верификации программ, внешняя среда которых непредставима в виде автоматов, который рассмотрен на примере использования в качестве внешней среды неограниченного клетчатого поля. При этом была выполнена верификация 800 решений задачи поиска пути агентом с O(1)памяти на неограниченном клетчатом поле. В результате верификации удалось доказать корректность 231 программы. Статья с описанием предложенного подхода принята на конференцию IBM Haifa Verification Conference 2014 [87].
Еще по теме Результаты верификации:
- Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014, 2014
- Результаты рентгеноструктурного анализа
- Результаты рентгенофазового анализа
- 5.2. Результаты исследования физико-механических свойств
- ПРОМЫШЛЕННАЯ АПРОБАЦИЯ РЕЗУЛЬТАТОВ ИССЛЕДОВАНИЙ
- Результаты исследования микроструктуры и рентгеноспектрального микроанализа
- Основные результаты и выводы
- Выводы по результатам исследования
- Результаты анализа гранулометрического состава
- Результаты исследования морфологии и элементного состава
- Основные результаты и выводы
- Основные результаты и выводы
- Результаты рентгенофазового анализа закаленных образцов порошковых низколегированных сталей
- Основные результаты исследования изложены в следующих публикациях автора: