Редактирование: ВПнМ, примеры задач/Задача 4
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 3: | Строка 3: | ||
# Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt. | # Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt. | ||
+ | |||
# В модели не должно быть недостижимого кода (unreachable code). | # В модели не должно быть недостижимого кода (unreachable code). | ||
+ | |||
# Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt | # Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt | ||
+ | |||
# В модели не должно быть циклов бездействия (non-progress cycles), за исключением: | # В модели не должно быть циклов бездействия (non-progress cycles), за исключением: | ||
+ | |||
## цикла, связанного с бесконечным выполнением моделируемой функции | ## цикла, связанного с бесконечным выполнением моделируемой функции | ||
+ | |||
## циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml. | ## циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml. | ||
+ | |||
# Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl. | # Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl. | ||
+ | |||
+ | |||
a. В случае, если модель пришлось изменить: | a. В случае, если модель пришлось изменить: | ||
+ | |||
* описать в теле письма, почему спецификация не выполняется на исходной модели; | * описать в теле письма, почему спецификация не выполняется на исходной модели; | ||
+ | |||
* описать в теле письма, как изменилась модель и почему; | * описать в теле письма, как изменилась модель и почему; | ||
+ | |||
* описать в теле письма, почему новая модель адекватна; | * описать в теле письма, почему новая модель адекватна; | ||
+ | |||
* приложить контрпример, выданный pan, в файле counterexample.txt; | * приложить контрпример, выданный pan, в файле counterexample.txt; | ||
+ | |||
* приложить исходную и изменённую модели в файлах model.prm и new_model.prm; | * приложить исходную и изменённую модели в файлах model.prm и new_model.prm; | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
b. В случае, если спецификация не выполняется на модели: | b. В случае, если спецификация не выполняется на модели: | ||
+ | |||
* приложить контрпример, выданный pan, в файле counterexample.txt; | * приложить контрпример, выданный pan, в файле counterexample.txt; | ||
+ | |||
* построить по контрпримеру Spin контрпример на исходной программе; | * построить по контрпримеру Spin контрпример на исходной программе; | ||
+ | |||
* убедиться в том, что контрпример на исходной программе выполняется; | * убедиться в том, что контрпример на исходной программе выполняется; | ||
+ | |||
* приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. | * приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
c. В случае, если изменения в модели не потребовались и спецификация выполняется: | c. В случае, если изменения в модели не потребовались и спецификация выполняется: | ||
+ | |||
* приложить модель в файле model.prm; | * приложить модель в файле model.prm; | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
Во всех случаях письмо должно удовлетворять требованиям: | Во всех случаях письмо должно удовлетворять требованиям: | ||
+ | |||
* письмо написано в формате plain/text без html; | * письмо написано в формате plain/text без html; | ||
+ | |||
* в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r). | * в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r). | ||
+ | |||
* к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt | * к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt | ||
Строка 125: | Строка 155: | ||
fi; | fi; | ||
} | } | ||
+ | :: (msg == SYS_END) -> break; | ||
:: else -> skip; | :: else -> skip; | ||
fi; | fi; | ||
Строка 192: | Строка 223: | ||
* Добавлен assert для проверки спецификации | * Добавлен assert для проверки спецификации | ||
* Добавлены метки progress для внешних циклов у каждого процесса, так как они должны быть бесконечными | * Добавлены метки progress для внешних циклов у каждого процесса, так как они должны быть бесконечными | ||
- | * Добавлены глобальные переменные и их изменение для верификации модели с использованием LTL | + | * Добавлены глобальные переменные и их изменение для верификации модели с использованием LTL |
- | + | <pre>#define OK 0 | |
- | + | #define NOT_OK 1 | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | #define SYS_IRQPOLICY 1 | |
- | + | #define SYS_IRQENABLE 2 | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | int DspVersion[2]; | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | chan to_kernel_channel = [0] of {byte}; | |
- | + | chan from_kernel_channel = [0] of {byte}; | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | <strong>bool call_irqenable;</stron> | |
- | + | active proctype kernel() | |
- | + | { | |
- | + | int msg; | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | <strong>progress:</strong> | |
- | < | + | do |
- | + | :: to_kernel_channel?msg -> | |
- | + | { | |
- | + | ||
- | < | + | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
if | if | ||
- | :: (! ( | + | :: (msg == SYS_IRQPOLICY) -> |
- | :: ( | + | { |
+ | if | ||
+ | :: from_kernel_channel!OK; | ||
+ | :: from_kernel_channel!NOT_OK; | ||
+ | fi; | ||
+ | } | ||
+ | :: (msg == SYS_IRQENABLE) -> | ||
+ | { | ||
+ | <strong>assert(DspVersion[0] < 4);</strong> | ||
+ | if | ||
+ | :: from_kernel_channel!OK; | ||
+ | :: from_kernel_channel!NOT_OK; | ||
+ | fi; | ||
+ | } | ||
+ | :: (msg == SYS_END) -> break; | ||
+ | :: else -> skip; | ||
fi; | fi; | ||
- | + | } | |
- | + | od; | |
- | } | + | } |
- | + | active proctype dsp_init() | |
+ | { | ||
+ | <strong>progress:</strong> | ||
+ | do | ||
+ | :: | ||
+ | byte result; | ||
- | + | DspVersion[0] = 0; | |
- | + | DspVersion[1] = 0; | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | + | if | |
- | + | :: DspVersion[0] = 0; | |
- | + | :: DspVersion[0] = 1; | |
+ | :: DspVersion[0] = 5; | ||
+ | fi; | ||
- | + | if | |
- | + | :: DspVersion[1] = 0; | |
- | + | :: DspVersion[1] = 1; | |
- | + | fi; | |
- | + | ||
- | + | if :: (DspVersion[0] < 4) -> | |
- | + | { | |
- | + | goto return; | |
- | + | } | |
- | + | :: else -> skip; | |
- | + | fi; | |
- | + | /* sys_irqsetpolicy(SB_IRQ, IRQ_REENABLE, &irq_hook_id); */ | |
+ | to_kernel_channel!SYS_IRQPOLICY; | ||
+ | from_kernel_channel?result; | ||
+ | if | ||
+ | :: (result != OK) -> | ||
+ | { | ||
+ | goto return; | ||
+ | } | ||
+ | :: else -> skip; | ||
+ | fi; | ||
- | + | /* sys_irqenable(&irq_hook_id) */ | |
- | </ | + | <strong>call_irqenable = true;</strong> |
+ | to_kernel_channel!SYS_IRQENABLE; | ||
+ | from_kernel_channel?result; | ||
+ | <strong>call_irqenable = false;</strong> | ||
- | = | + | if :: (result != OK) -> |
+ | { | ||
+ | goto return; | ||
+ | } | ||
+ | :: else -> skip; | ||
+ | fi; | ||
- | + | return: | |
- | + | skip; | |
+ | od; | ||
+ | }</pre> | ||
- | + | ==== Проверка свойства отсутствия тупиков ==== | |
- | + | ==== Проверка на наличие недостижимого кода ==== | |
- | + | ||
- | + | ||
- | + | ==== Проверка выполнения assertions ==== | |
- | + | ||
- | + | ||
- | + | ===== Построение контрпримера ===== | |
- | + | ||
- | + | ||
- | + | ==== Проверка на отсутствие циклов бездействия ==== | |
- | + | ||
- | + | ==== Формулирование формулы LTL ==== | |
- | + | ||
- | + | ||
- | + | ||
- | + | ||
- | === | + | |
- | + | ||
- | + | === Дополнительные материалы для выполнения задания === | |
- | + | ==== Скрипт для генерации файлов, необходимых в задании, на основании моделей ==== | |
- | + | Данный скрипт генерирует файлы assert_out.txt, ver_out.txt, nonprogress_out.txt, safety_out.txt, spec.ltl на основании | |
- | + | ||
{{Курс ВПнМ}} | {{Курс ВПнМ}} |