<<
>>

Инструментальное средство Stater

Начиная с 2014 года Staterиспользуется вместо Converterв учебном процессе на кафедре «Компьютерные технологии». Функциональность Stater позволяет упростить верификацию, так как в нём можно сначала строить системы автоматов, а после этого их верифицировать.

4.2.1. Загрузка из XML-файла

Инструментальное средство Staterбыло использовано при разработке программы AntsysEditorв ООО «СТЦ». AntSysEditorпредназначен для редактирования информации о структуре антенн, которая хранится в XML- файлах в следующем формате:

1. Внешний тег содержит все остальные и сообщает номер версии соответствующей программы, с помощью которой данный XML- файл был создан. Этот тэг только один в файле.

2. Второй по вложенности тег содержит общую информацию для всей антенны: Index, id, Kind, ASName, BegFreq, EndFreq, Roll, Pitch, Yaw, Latitude, Longitude и Height. Бывает только один в файле.

3. Самым глубоким по вложенности тегом, является тег , который содержит информацию непосредственно о конкретном антенном элементе: id, x, y, z и phase. Число таких тегов равно числу используемых антенных элементов.

Верификация осуществлялась для автомата ALoader, который реализует следующий алгоритм обработки XML-файлов данного формата:

1. Если приходит тег , то автомат переходит в состояние _Kind_.

2. Далее обрабатываются все поля тэга. Например, если тэг содержит параметр Id, то вызывается функция SetId, которая устанавливает значение Id, и автомат переходит в состояние _Kind_

3. Если приходит тег , то вызывается функция создания нового объекта NewAE, и автомат переходит в состояние AE.

4. В состоянии AE обрабатываются поля, соответствующие данному тегу. Например: приходит параметр id, вызывается функция SetAEid, которая устанавливает значение id у объекта, и автомат переходит в состояние AE.

5. Если автомат находится в состоянии AE и приходит закрывающий тег , то вызывается функция добавления элемента AddAE, и автомат переходит в состояние _Kind_.

Автомат ALoader приведён на рисунке 4.2.1.1.

Рисунок 4.2.1.1. Автомат ALoader

Приведём LTL-спецификацию для этого автомата.

Формулаf0.«Нельзя обрабатывать тег , пока нет тега ».

( {loader.AE}) -> (!{loader.AE} U {loader.kind})

Формула fl.«Если объект AE создан, то нельзя обрабатывать следующий тег до добавления объекта».

[](({loader._Kind_} &&{loader.ae}) -> (!{loader._Kind_} U

{loader.ae}))

Формула f2.«Если обрабатываем значение x объекта AE, то обязательно вызовется функция установки х». Можно написать аналогичные формулы для каждого элемента каждого тега.

[](({loader.AE} &&{loader.x}) -> ({loader.SetAEX} U {loader.AE}))

После формализации спецификации была выполнена верификация. Посроенная при помощи Stater Spin-модель и вывод Spinприведены в Приложении А. Из изложенного следует, что в рассмотренной задаче верифицируемые свойства выполнены.

4.2.2. Игра Turtleball

При помощи инструментального средства Starterпроверифицирована также логика в игре «Turtleball HD».Смысл игры состоит в том, что прямоугольному полю, ограниченному стенами, катятся шарики, а игрок должен при помощи стен отсекать части поля от шариков. Стена растёт от места, по которуму кликнул игрок, в две стороны (либо вертикально, либо горизонтально), пока не дорастёт до другой стены. Шарик ударился о строящуюся стену, то игрок теряет «жизнь», а стена уничтожается. Замкнутая стенами часть поля, в которой нет шариков, заполняется. Цель игрока состоит в том, чтобы заполнить 70% поля.

Автомат AWall описывает логику пересечения стен с шариками:

1. Изначально автомат находится в состоянии Start.

2. В зависимости от того, как растёт стена, вертикально или горизонтально, автомат переходит в состояние GrowVertical или GrowHorizontal.

3. Если автомат находится в одном из предыдущих состояний и ему приходит событие пересечения стены с шариком, то выполняется функция KillAll, и автомат переходит в состояние Kill.

Если пришло событие, что стена установилась, то автомат переходит в состояние Wall.

4. В состоянии Kill, если приходит событие reset, то стена сбрасывается.

Автомат AWall приведён на рисунке 4.2.2.1.

Рисунок 4.2.2.1. Автомат AWall

Приведём LTL-спецификацию для этого автомата

Формула f0.«Если шарик ударился о стену, то она когда-то начнёт строиться заново».

[] (({awall.Kill}) -> ({awall.Start}))

Формула fl.«Если шарик не ударился о стену, то она построится».

[]((!( {awall._Kill_})) -> ( {awall.Wall}))

Автомат APlatform описывает логику роста обеих стен при нажатии на экран:

1. Изначально автомат находится в состоянии Start. Когда игрок кликает на экран, автомат переходит в состояние роста двух стен Grow2Walls.

2. Из состояния Grow2Walls, если ничего не произошло и приходит событие обновления, автомат переходит в состояние Grow2Walls, вызвав функции DoGrowWallOne и DoGrowWallOther. Если приходит событие остановки роста стены StopOneSide или StopOtherSide, то автомат переходит в состояние GrowOtherWall или GrowOneWall, соответственно.

3. Из состояния GrowOtherWall при событии обновления автомат переходит в состояние GrowOtherWall, вызвав функцию DoGrowOtherWall. Если приходит событие StopOtherSide, то автомат переходит в начальное состояние Start.

4. Из состояния GrowOneWall при событии обновления автомат переходит в состояние GrowOneWall, вызвав функцию DoGrowOneWall. Если приходит событие StopOneSide, то автомат переходит в начальное состояние Start.

Рисунок 4.2.2.2. Автомат APlatform

Приведём LTL-спецификацию для этого автомата.

Формула f0.«Стены растут вместе либо бесконечно, либо будут расти до остановки роста одной из них».

[](({aplatform.Grow2Walls}) -> (({aplatform.Grow2Walls} U ({aplatform.GrowOneWall} || {aplatform.GrowOtherWall})) || []({aplatform.Grow2Walls})))

Формула fl.

«Если остановилась стена One,то далее будет расти только стена Other».

[](({aplatform.GrowOtherWall}) -> (({aplatform.GrowOtherWall} U {aplatform.Start}) || []({aplatform.GrowOtherWall})))

Формула f2. «Если обе стены были когда-то остановлены, то автомат побывал в начальном состоянии».

(( {aplatform.StopOneSide}) &&( {aplatform.StopOtherSide}))

-> ( {aplatform.Start})

Формулаf3.«Если одна стена начала расти, то сначала росли обе».

( ({aplatform.GrowOtherWall} || {aplatform.GrowOneWall})) -> (!({aplatform.GrowOtherWall} &&{aplatform.GrowOneWall}) U {aplatform.Grow2Walls})

После формализации спецификации была выполнена верификация. Посроенная при помощи Stater Spin-модель и вывод Spinприведены в Приложении Б. Из изложенного следует, что в рассмотренной задаче верифицируемые свойства выполнены.

4.2.3. Программа Memory cardsдля запоминания иностранных слов

Инструментальное средство Staterбыло также использовано автором для написания коммерческого программного обеспечения Memory cardsдля обучения иностранному языку. Оно доступно по адресу http://prognotes.ru/glubina/memory-cards/. Эта программа является электронной версией карточек для запоминания иностранных слов (на одной стороне карточки записано слово, а на другой перевод). Будем верифицировать автомат Mnemo, который реализует алгоритм показа карточек. Приведём описание этого алгоритма:

1. Вся колода карточек делится на несколько пачек (без участия автомата).

2. Пользователю показывается первая карточка функцией GotoFirstCard

(автомат вызывает эту функцию, но она определена вне автомата).

3. Показ карточки осуществляется следующим образом:

3.1. Показывается лицевая сторона карточки. По нажатию на кнопку «Перевернуть», карточка переворачивается, и показывается обратная сторона. После этого пользователь решает, правильно он вспомнил слово, или ошибся, и нажимает, соответственно кнопку «Верно» или «Неверно». После этого пользователю 87

показывается следующая карточка функцией GetNextCard (автомат вызывает эту функцию, но она определена вне автомата).

4. Для каждой пачки карточек:

4.1. Первый проход: запоминание. Пачка перемешивается, и показываются по очереди все карточки из пачки. Когда пачка заканчивается, в автомат приходит событие pack_is_over. Определение конца пачки происходит вне автомата.

4.2. Второй проход: повторение. Пачка перемешивается, и показываются все карточки по очереди. При этом если пользователь отметил, что он ошибся на некоторой карточке, то она возвращается обратно в пачку.

4.3. Третий проход аналогичен второму, но все карточки показываются с обратной стороны.

4.4. Осуществляется переход к следующей пачке.

5. Алгоритм заканчивает работу и переходит в начальное состояние, когда закончились пачки.

Автомат Mnemo приведён на рисунке 4.2.2.1.

Рисунок 4.2.2.1. Автомат Mnemo

Автомат содержит следующие переменные:

• param int8 nPacks = 0;

• param int8 nPasses = 4;

• int16 iPass = 0;

• int8 packCount = 0 ;

Состояние state0 - начальное состояние автомата. В этом состоянии автомат ждёт начала работы. Состояние ConnForward соответствует шагу 4.1 алгоритма. Состояние FRepF - шагу 4.2, а состояние BRepF - шагу 4.3. Переход из состояния BRepF в состояние ConnForward осуществляет шаг 4.4.

Приведём LTL-спецификацию для этого автомата.

Формула f0. «Если в процессе повторения пользователь отметил, что он не угадал слово на карточке, то эта карточка будет положена в оставшуюся часть пачки ещё раз до того, как будет выбрана следующая карточка из пачки». Повторение карточек происходит в состояниях mnemo.FRepF и mnemo.BRepF. «Пользователь отметил, что не угадал слово на карточке» - это событие mnemo.wrong. «Вернуть карточку в оставшуюся часть пачки» - mnemo.ReturnCurCard. «Выбрать следующую карточку» -

mnemo.GetNextCard. В результате может быть записана следующая формула:

[] ( (({mnemo.FRepF} || {mnemo.BRepF}) &&{mnemo.wrong} &&

(!({mnemo.ReturnCurCard})) &&(!({mnemo.GetNextCard }))) -> ((!{mnemo.GetNextCard}) U {mnemo.ReturnCurCard}))

Формула fl.

«Если пользователь отметил, что он угадал либо не угадал слово на карточке, то будет выдана следующая карточка:

[](({mnemo.wrong} || {mnemo.correct}) -> (({mnemo.GetNextCard})))

Формула f2. «Алгоритм всегда сможет закончить работу и вернуться в состояние ожидания»:

[]{mnemo.state0}.

Эта формула не должна выполняться, так как вычисление конца пачки находится вне автомата, и если автомату не будет приходить событие pack_is_over, то он не сможет завершить работу. Это подтверждается результатом верификации (листинг 4.2.2.1), который выдаёт следующий контрпример: в автомат приходит событие init_event, автомат переходит в состояние ConnForward, после этого в бесконечном цикле в автомат приходит событие correct.

Листинг 4.2.2.1. Результат верификации свойства []{mnemo.state0}

There are errors. Counterexample:

mnemosource sent _init_event_ mnemosource sent _init_event_ mnemo.nPacks = 255

mnemo.nPasses = 255

mnemo.iPass = 0

mnemo.packCount = 0

mnemo.state = Mnemo.state0

mnemo. event_happened: _init_event_

mnemo.LoadPack()

mnemo.GotoFirstCard()

mnemosource sent _init_event_

mnemo.nPacks = 255

mnemo.nPasses = 255

mnemo.iPass = 0

mnemo.packCount = 0

mnemo.state = Mnemo.ConnForward

mnemosource sent _correct_

mnemo.nPacks = 255

mnemo.nPasses = 255

mnemo.iPass = 0

mnemo.packCount = 0

mnemo.state = Mnemo.ConnForward

mnemo. event_happened: _correct_

mnemo.GetNextCard()

mnemosource sent _correct_

mnemo.nPacks = 255

mnemo.nPasses = 255

mnemo.iPass = 0

mnemo.packCount = 0

mnemo.state = Mnemo.ConnForward mnemo. event_happened: _correct_ mnemo.GetNextCard()

Формулы f3 - f5.Заменим формулу f2тремя другими формулами f3 - f5,

которые должны выполняться:

f3: [](( {mnemo.ConnForward} &&{mnemo.pack_is_over}) -> ( {mnemo.FRepF}))

f4: [](( {mnemo.FRepF } &&{mnemo.pack_is_over} &&(mnemo.iPass ( {mnemo.BRepF}))

f5: [](({mnemo.BRepF } &&{mnemo.pack_is_over} && (mnemo.packCount >= mnemo.nPacks - 1) && (mnemo.iPass (

{mnemo.state0}))

Формула f6.«Во время шагов 4.2 - 5 алгоритма значение iPass не превосходит nPasses».

[](({mnemo.FRepF} || {mnemo.BRepF}) -> mnemo.iPass

<< | >>
Источник: Лукин Михаил Андреевич. Верификация автоматных программ. Диссертация на соискание ученой степени кандидата технических наук. Санкт-Петербург - 2014. 2014

Еще по теме Инструментальное средство Stater:

  1. Коммутационные средства матричных СБИС-мультипроцессоров
  2. СПИСОК ЛИТЕРАТУРЫ
  3. ВВЕДЕНИЕ
  4. Анализ химического состава
  5. II.МЕТОДЫ ГОСУДАРСТВЕННОГО УПРАВЛЕНИЯ.
  6. 2.ПОНЯТИЕ И ОБЩАЯ ХАРАКТЕРИСТИКА ГОСУДАРСТВЕННОГО УПРАВЛЕНИЯ
  7. Принципы банковского надзора
  8. 2. Производство по делам об административных правонарушениях
  9. 3.1. Пруденциальный банковский надзор: понятие и взаимосвязь с государственным финансовым контролем
  10. 30. Меры оперативного воздействия на правонарушителя.
  11. 19. Понятие и виды объектов гражданского права.
  12. СОДЕРЖАНИЕ