Предлагаемый подход к верификации
Корректность работы агента следует из двух утверждений: «Для любого поля если цель достижима, то агент за конечное время достигнет её и выполнит действие “report reached”» и «Для любого поля если цель
недостижима, то агент за конечное время выполнит действие “report unreachable”».
Сложность верификации состоит в том, что по условию задачи размер поля не ограничен. Автору неизвестно, как неограниченное поле закодировать при помощи темпоральных формул или автомата с конечным числом состояний.Для решения этой задачи автором был предложен подход, состоящий из следующих шагов:
1. Построить гипотезу об алгоритме, который реализует программа.
2. Построить модель (возможно, неполную и недетерминированную) программы и внешней среды и множество формул, которые вместе с моделью будут использованы верификатором для доказательства, что данная программа соответствует гипотезе.
3. Формально доказать как теорему, что если программа соответствует гипотезе, то она корректна.
4. Запустить верификатор на всех автоматах, используя модель и формулы из шага 2. Программа, которая успешно прошла верификацию, корректна.
В настоящей главе предложенный подход будет шаг за шагом проиллюстрирован на примере верификации 800 автоматных программ, каждая из которых решает задачу, описанную в разделе5.1.
5.3.
Еще по теме Предлагаемый подход к верификации:
- Основные соотношения (бескоординатный подход)
- Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014, 2014
- Структурная модель устройства коммутации с параллельноконвейерной диспетчеризацией пакетов
- Выводы по результатам исследования
- § 2. Понятие и функции нотариата
- ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ
- О применяемых методиках расчета ширины раскрытия нормальных трещин
- Осокина Г. Л., Галковская Н.Г., Бурматнова .В., Кузьмина В.А., Барсукова Т.В. Практикум по арбитражному процессу / отв. ред. Н.Г. Галковская. - Томск : Издательский Дом Томского государственного университета,2018. - 142 с., 2018
- Задачи исследования
- Оценка эффективности методов несовершенного хеджирования опционных позиций на российском фондовом рынке
- Основные результаты и выводы
- ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ
- Рекомендации по конструированию балок трапециевидного поперечного сечения
- Право административных процедур и административно-процессуальное право в государствах Центральной Азии — краткий обзор современного состояния
- 2.ПОНЯТИЕ И ОБЩАЯ ХАРАКТЕРИСТИКА ГОСУДАРСТВЕННОГО УПРАВЛЕНИЯ
- Введение
- Методика исследования характеристик коммутационного устройства