Верификация
Для верификации предназначено дополнение SpinVeriff.Верификация проводится при помощи инструментального средства Spin.Для этого, как описано в разделе 3.2, строится модель распределенной системы автоматов на языке Promela.На рисунке 3.7.3.1 показаны настройки дополнения SpinVeriff.
В поле «LTL formulae»вводятся одна или несколько LTL-формул (по одной на каждую строку).
Формулы имеют формат Spinза исключением того, что атомарные высказывания записываются в фигурных скобках.
Рисунок 3.7.3.1. Настройки верификатора
Атомарные высказывания могут быть следующих видов:
1. machineName . exx - в автомат machineNameпришло событие exx.
2. machineName . sxx - автомат machineNameперешел в состояние sxx.
3. machineName.Function - автомат machineNameвызвал выходное воздействие Function.
4. machineName->nestedMachine - автомат machineNameдошёл до вложенного автомата nestedMachine.
5. machineName || forkMachine - автомат machineNameзапустил автомат forkMachine.
6. machineName.variable OP value сравнивает переменную или элемент массива экземпляра machineName автомата MachineType со значением value. OP - оператор сравнения (>, =,
Еще по теме Верификация:
- Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014, 2014
- Некоторые вопросы реформирования административного правосудия в Кыргызской Республике
- Тема: ПРОИЗВОДСТВО В СУДЕ КАССАЦИОННОЙ ИНСТАНЦИИ
- О понятии финансового опциона
- § 2. Понятие и функции нотариата
- ГРИБОВСКАЯ Наталья Юрьевна. ЛЕКСИКА ТВЕРСКИХ ГОВОРОВ, ХАРАКТЕРИЗУЮЩАЯ ЧЕЛОВЕКА (СЕМАНТИКО-МОТИВАЦИОННЫЙ АСПЕКТ). Автореферат диссертации на соискание ученой степени кандидата филологических наук. Тверь - 2019, 2019
- 26. Возникновение гражданских правоотношений не предусмотренных в ГК
- П.2 Частотная зависимость условий существования объемных и эванесцентных волн TM- (ТЕ-) типа и соответствующих типов сечений ПВВ в коллинеарной фазе скомпенсированого ЛО АФМ с ЦАС. Полярная MOK
- 59 ВИДЫ И ФОРМЫ ДОГОВОРА.
- Микрополе «Речевая деятельность»