WWW.DISS.SELUK.RU

БЕСПЛАТНАЯ ЭЛЕКТРОННАЯ БИБЛИОТЕКА
(Авторефераты, диссертации, методички, учебные программы, монографии)

 

Материал опубликован в тезисах научно-технической конференции

«Научное программное обеспечение в образовании и научных

исследованиях». СПбГУ ПУ. 2008, с. 36–40.

В. С. Гуров, Б. Р. Яминов

ТЕХНОЛОГИЯ ВЕРИФИКАЦИИ АВТОМАТНЫХ МОДЕЛЕЙ

ПРОГРАММ БЕЗ ИХ ТРАНСЛЯЦИИ ВО ВХОДНОЙ ЯЗЫК

ВЕРИФИКАТОРА

Автоматные модели программ [1] широко используются для создания реактивных управляющих систем [2] поскольку автоматы позволяют наглядно и надежно представлять поведение системы. Реактивные системы часто используются в областях, в которых требуется безотказная работа и цена ошибки чрезвычайно велика. По этой причине возникла необходимость в автоматической проверке соблюдения заданных свойств автоматной программой.

Одним из методов для автоматической проверки программ является Model checking [3, 4]. Это автоматизированный подход, позволяющий для заданной модели поведения системы с конечным (возможно, очень большим) числом состояний и логического свойства (требования) проверить, выполняется ли это свойство в рассматриваемых состояниях модели.

Проверяемые свойства формулируются в темпоральной логике, позволяющей задавать не только мгновенное состояние системы, но и историю развития системы во времени.

Идею метода Model checking реализуют специальные программы – верификаторы. Такая программа получает на вход модель, описанную на входном языке верификатора, и свойство, которое проверяется (возможно, на другом языке). На выходе программа формирует либо сообщение о том, что указанное свойство на заданной модели выполняется, либо набор действий (сценарий), приводящий к его нарушению.

Существует большое количество верификаторов, в том числе, и с открытыми кодами. Поэтому имеет смысл воспользоваться одним из уже существующих. Для того чтобы проверять свойства автоматных моделей с помощью уже существующего верификатора требуется осуществлять две операции:

• транслировать автоматную модель во входной язык верификатора;

• при получении сценария ошибки, транслировать его обратно в автоматную модель.

Существует несколько работ [4, 5], в которых упомянутые операции выполнялись вручную. Однако до сих пор неизвестны автоматические верификаторы автоматных моделей программ.





Цель настоящей работы – создать автоматический верификатор программ рассматриваемого класса.

Трансляция автоматной модели во входной язык верификатора и обратно порождает ряд проблем. Во-первых, возможно возникновение наведенных ошибок – ошибок, которых не было в исходной модели, но они появились в верифицируемой модели из-за недостаточно корректной трансляции. Вовторых, порождаются «лишние» состояния, которые не влияют на результат верификации, но увеличивают объем работы верификатора.

В данной работе предлагается новый подход к решению задачи верификации автоматных моделей программ. Его идея заключается в том, чтобы миновать этап трансляции и позволить верификатору осуществлять переходы прямо в автоматной модели. Такой подход позволяет решить перечисленные выше проблемы.

Для реализации идеи требуется верификатор с расширяемым входным языком, для которого кроме стандартных типов объектов (булев тип, целочисленный, строковый и т.д.) можно создавать более сложные и абстрагированные структуры и специфицировать их свойства. Это позволит ограничить дробление модели на мелкие элементарные состояния.

Кроме того, требуется интерпретатор автоматной модели – инструментальное средство, которое по событиям осуществляет переходы между состояниями в автомате, вычисляет значения условий на переходах и запускает вложенные автоматы. Верификатор будет использовать это средство для перемещения между состояниями в автоматной модели.

В качестве интерпретатора было выбрано инструментальное средство Unimod [6, 7], которое предназначено для создания и интерпретации программ, основанных на автоматном подходе. Это средство позволяет создавать реактивные системы, в которых выделяются:

1. Источники событий – сущности, которые поставляют автомату события для обработки. Это «сенсоры» реактивной системы.

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

Автоматы могут иметь гиперсостояния и быть вложены в состояния других автоматов. Действия могут помечать состояния и/или переходы.

3. Объекты управления – сущности, у которых можно вызывать действия и запрашивать значения предикатов.

В качестве верификатора с расширяемым входным языком выбрано средство Bogor [8, 9]. Инструментальные средства Bogor и Unimod реализованы на одном языке программирования (Java). Это позволяет их весьма легко интегрировать.

В данной работе было создано расширение входного языка Bogor в виде нового класса – AutomataModel. Объект этого класса представляет собой автоматную модель. Для него задано лишь одно действие: step (шаг), которое совершает обработку очередного события в модели. Также у объекта этого класса можно получать различную информацию о состояниях автоматов, вызванных в ходе шага выходных воздействиях и других свойствах, которые могут понадобиться для формулировки верифицируемого требования к модели.





Глобальное состояние объекта нового класса кодируется как набор состояний каждого автомата. Это означает, что из одинакового набора состояний автоматов в модели должно следовать одинаковое ее поведение на любые воздействия. Данное утверждение может нарушаться, если часть логики реактивной системы хранится в объектах управления. К примеру, в одном и том же наборе состояний автоматов некоторый флаг внутри объекта управления может быть разным, что приведет к разному поведению. Методы решения задачи для такого случая будут описаны в конце настоящей работы.

За счет создания класса AutomataModel спецификация автоматной модели во входном файле верификатора Bogor сводится всего лишь к одному бесконечному циклу, в котором совершается шаг автоматной модели. Сама модель инициализируется из Unimod-файла. С точки зрения верификатора, обработка одного события в автоматной модели происходит атомарно.

Для решения задачи верификации автоматных моделей остается записать проверяемые требования. Это можно сделать во входном файле Bogor в виде автомата Бюхи [3], либо в виде формулы темпоральной логики LTL, используя в утверждениях методы класса AutomataModel.

Созданный верификатор был апробирован на нескольких примерах и успешно доказывал верные утверждения о моделях и выдавал сценарии нарушений для неверных утверждений. Приведем один из таких примеров – модель дверей лифта (см. рисунок).

При открытии дверей может произойти ошибка (e4). При закрытии двери могут встретить препятствие (e3), в случае чего они снова открываются. Верификатору подавалась на вход модель дверей лифта и перечисленные ниже утверждения.

• При отсутствии ошибки (e4) для любой «справедливой» истории [3] состояние Opened (Открыта) посещается бесконечное количество раз.

Справедливая история означает, что любое ожидаемое событие когданибудь произойдет, и модель не остановится навсегда в состоянии, из которого есть выход по некоторому событию. Результат верификации данного утверждения – «Выполняется».

• При отсутствии ошибки (e4) для любой «справедливой» истории состояние Closed (Закрыта) посещается бесконечное количество раз.

Результат верификации – «Нарушается». Верификатор выводит контрпример в виде пути, когда при каждой попытке закрыться дверь встречает препятствие (e3).

В данной работе при верификации реактивных систем предполагается, что в объектах управления нет логики. Источники событий и объекты управления отключаются от системы, и работа проводится с «изолированной»

автоматной моделью. Однако в ряде случаев логика может быть также и в объектах управления. К примеру, может существовать зависимость между входными и выходными воздействиями объекта, которая не будет учтена при верификации. Это приведет к несуществующим историям развития, а значит, возможно, к наведенным ошибкам.

Тем не менее, эта проблема разрешима.

1. Можно вручную формулировать такие зависимости (ограничения) в темпоральной логике и добавлять их в верифицируемую формулу для исключения невозможных сценариев ошибок.

2. В будущем предполагается создание формальной системы задания пред- и постусловий для действий объектов управления, для того чтобы автоматически учитывать указанные зависимости при верификации.

Данная работа показывает, как можно весьма просто и эффективно верифицировать автоматные модели.

Работа выполнена как дополнение к инструментальному средству Unimod. Это позволяет получить единое средство для создания, интерпретации и верификации реактивных систем.

Источники 1. Шалыто А. А. Switch-технология. Алгоритмизация и программирование http://is.ifmo.ru/books/switch/l/ 2. Шалыто А. А., Туккель Н. И. SWITCH-технология – автоматный подход к созданию программного обеспечения «реактивных» систем // Программирование. 2001. № 5. http://is.ifmo.ru/works/switch/l/ 3. Clarke E. M., Grumberg O., Peled D. A. Model checking. The MIT Press. 2000.

4. Вельдер С. Э., Шалыто А. А. Введение в верификацию автоматных http://is.ifmo.ru/download/modelchecking.pdf 5. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ. Ярославский государственный университет им.

П.Г. Демидова.

6. UniMod project. http://unimod.sourceforge.net/ 7. Гуров В., Мазин М., Нарвский А., Шалыто А. UML. SWITCH-технология.

http://is.ifmo.ru/works/uml-switch-eclipse/ 8. Bogor website. http://bogor.projects.cis.ksu.edu/ 9. Robby, Dwyer M., Hatcliff J. Bogor: A Flexible Framework for Creating http://projects.cis.ksu.edu/docman/view.php/8/125/SAnToS-TR2006-2.pdf

 
Похожие работы:

«Техническое описание Использования языка Cg для профессиональной работы Использование языка Cg для профессиональной работы: Революционная производительность “Совместное представление NVIDIA Quadro FX и визуализации на базе графического процессора в рамках SolidWorks стало революционным событием. Когда-то разработчики спорили по поводу превосходства 3D над 2D; тогда монолитные модели пришли на смену каркасным; изображения с тенями сменили черно-белые; затем цветные монолитные модели заменили...»

«ПРОГРАММА РАЗВИТИЯ ГОСУДАРСТВЕННОГО ОБРАЗОВАТЕЛЬНОГО УЧРЕЖДЕНИЯ ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ ИРКУТСКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНИЧЕСКИЙ УНИВЕРСИТЕТ НА 2010–2019 гг. ОБРАЗЦЫ ПАСПОРТОВ НАУЧНО-ИССЛЕДОВАТЕЛЬСКОЙ ЛАБОРАТОРИИ И УЧЕБНО-ИССЛЕДОВАТЕЛЬСКОЙ ЛАБОРАТОРИИ Выпуск 9 2012 Программа развития государственного образовательного учреждения высшего профессионального образования Иркутский государственный технический университет на 2010–2019 гг.: Образцы паспортов научноисследовательской...»

«Бизнес-план Производство чистой питьевой воды 2012 год 2 Содержание Список таблиц Список рисунков Резюме Введение Концепция проекта 1. 2. Описание продукта (услуги) 3. Программапроизводств 4. Маркетинговый план 4.1 Описание рынка продукции (услуг) 4.3 Стратегия маркетинга 5. Техническое планирование Средства доставки воды 6. Организация, управление и персонал 7. Реализация проекта 8. Эксплуатационные расходы 9. Общие и административные расходы 10. Потребность в капитале и финансирование 11....»

«Министерство образования Республики Беларусь Учебно-методическое объединение по образованию в области культуры и искусств УТВЕРЖДАЮ Первый заместитель Министра образования Республики Беларусь _А. И. Жук _2012 г. Регистрационный № ТД-/тип. УПРАВЛЕНИЕ КАЧЕСТВОМ И СЕРТИФИКАЦИЯ Типовая учебная программа для высших учебных заведений по направлению специальности 19 01 01-05 Дизайн (костюма и тканей) СОГЛАСОВАНО СОГЛАСОВАНО Заместитель председателя Начальник Управления высшего и концерна Беллегпром...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Государственное образовательное учреждение высшего профессионального образования Уфимский государственный нефтяной технический университет УТВЕРЖДАЮ Ректор ГОУ ВПО УГНТУ Д.т.н., профессорА.М.Шаммазов 20_г. ОСНОВНАЯ ОБРАЗОВАТЕЛЬНАЯ ПРОГРАММА ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ Направление подготовки 230100 ИНФОРМАТИКА И ВЫЧИСЛИТЕЛЬНАЯ ТЕХНИКА Профиль подготовки ИНФОРМАЦИОННОЕ И ПРОГРАММНОЕ ОБЕСПЕЧЕНИЕ АВТОМАТИЗИРОВАННЫХ СИСТЕМ Квалификация...»

«Утверждаю Ректор МГТУ ГА _Б.П. Елисеев 20г. ОСНОВНАЯ ОБРАЗОВАТЕЛЬНАЯ ПРОГРАММА ВЫСШЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ Направление подготовки 162500 Техническая эксплуатация авиационных электросистем и пилотажно-навигационных комплексов Профиль подготовки Техническое обслуживание и ремонт авиационных электросистем и пилотажно-навигационных комплексов Квалификация (степень) бакалавр Форма обучения – очная Москва СОДЕРЖАНИЕ 1 Общие положения 1.1 Нормативные документы для разработки ООП ВПО по...»

«МКОУ Никольская ООШ Рабочая учебная программа по учебной дисциплине технология ( Автор: Роговцева Н.И.) для 2 класса УМК Школа России Программа составлена Щеновой Т.В. 2013 – 2014 учебный год. Пояснительная записка к тематическому планированию по технологии 2 класс Учебный предмет Технология имеет практикоРоль и место данной ориентированную направленность. Его содержание не только дисциплины в дает ребенку представление о технологическом процессе как образовательном совокупности применяемых при...»

«Областное государственное бюджетное образовательное учреждение среднего профессионального образования ния КОСТРОМСКОЙ ПОЛИТЕХНИЧЕСКИЙ КОЛЛЕДЖ КОСТРОМСКОЙ КОЛЛЕДЖ УТВЕРЖДАЮ Директор ОГБОУ СПО Костромской политехнический Костромской колледж колледж В.А. Смирнов _ 20 2013г. ОСНОВНАЯ ПРОФЕССИОНАЛЬНАЯ ОБРАЗОВАТЕЛЬНАЯ ПРОГРАММА СРЕДНЕГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ Специальность Гидрогеология и инженерная геология геология 130108 Квалификация: Техник-гидрогеолог Форма обучения: Очная Кострома...»

«Министерство образования и науки Российской Федерации Федеральное агентство по образованию РФ Владивостокский государственный университет экономики и сервиса _ ГИДРАВЛИКА Учебная программа курса по специальности 19060365 Сервис транспортных и технологических машин и оборудования (Автомобильный транспорт) Владивосток Издательство ВГУЭС 2008 1 ББК 22.253.3 Учебная программа по дисциплине Гидравлика составлена в соответствии с требованиями ГОС ВПО РФ ОПД.Ф.02.05. Предметом курса являются основные...»

«Министерство образования и науки Российской Федерации Бийский технологический институт (филиал) федерального государственного бюджетного образовательного учреждения высшего профессионального образования Алтайский государственный технический университет им. И.И. Ползунова УТВЕРЖДАЮ Заместитель директора по научной работе _ В.Н. Хмелев 2012 г. ОСНОВНАЯ ОБРАЗОВАТЕЛЬНАЯ ПРОГРАММА ПОСЛЕВУЗОВСКОГО ПРОФЕССИОНАЛЬНОГО ОБРАЗОВАНИЯ ПО СПЕЦИАЛЬНОСТИ 03.01.06 – Биотехнология (в том числе бионанотехнологии...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное автономное образовательное учреждение высшего профессионального образования СИБИРСКИЙ ФЕДЕРАЛЬНЫЙ УНИВЕРСИТЕТ Утверждаю Ректор СФУ _Е.А Ваганов _ 2012 г. Основная профессиональная образовательная программа послевузовского профессионального образования (аспирантура) по специальности 05.02.04 Трение и износ в машинах Присуждаемая ученая степень - кандидат технических наук Красноярск 2012 1. Общие положения...»

«Молодежный республиканский конкурс УМНИК инновационных идей по программе ПРОГРАММА проведения всероссийской научно-практической конференции ИННОВАЦИИ В НАУКЕ, ТЕХНИКЕ И ТЕХНОЛОГИЯХ Ижевск, 28-30 апреля 2014 УВАЖАЕМЫЕ КОЛЛЕГИ! Министерство образования и наук и Удмуртской Республики совместно с Федеральным государственным бюджетным учреждением Фонд содействия развитию малых форм предприятий в научно-технической сфере приглашает вас принять участие в работе Всероссийской научнопрактической...»

«ПАРТНЕР ОРГАНИЗАТОРЫ ПРОГРАММНЫЕ ПАРТНЕРЫ* *Полный список партнеров будет опубликован до 27 января Уникальная возможность погрузиться в мир технологий и стартапов, выбрать свою траекторию в инновационной экосистеме России, а также принять личное участие в проектировании и организации крупнейшей российской стартап конференции Startup Village. Лучшие идеи и решения будут использованы в В течение недели команды, составленные из числа Startup Village - 2014, а наиболее активные участников школы,...»

«СОДЕРЖАНИЕ ООП 1. Общие положения 1.1. Основная образовательная программа магистратуры Международное частное право. 1.2. Нормативные документы для разработки магистерской программы Международное частное право. 1.3. Общая характеристика магистерской программы Международное частное право. 1.3.1. Цель магистерской программы. 1.3.2. Срок освоения магистерской программы. 1.3.3. Трудоемкость магистерской программы. 1.4. Требования к уровню подготовки, необходимому для освоения магистерской программы....»

«Государственное образовательное учреждение высшего профессионального образования Липецкий государственный технический университет УТВЕРЖДАЮ Декан ЭФ _В.В.Московцев _2011 г. РАБОЧАЯ ПРОГРАММА ДИСЦИПЛИНЫ (МОДУЛЯ) АНАЛИЗ И ДИАГНОСТИКА ХОЗЯЙСТВЕННОЙ ДЕЯТЕЛЬНОСТИ Направление подготовки: 080200 Менеджмент Профиль подготовки: Производственный менеджмент Квалификация (степень) выпускника: бакалавр Форма обучения: очная г. Липецк – 2011 г. 1.Цели освоения дисциплины (модуля) Целями освоения дисциплины...»

«Учреждение образования БЕЛОРУССКИЙ ГОСУДАРСТВЕННЫЙ ТЕХНОЛОГИЧЕСКИЙ УНИВЕРСИТЕТ В. В. Мацкевич ТАМОЖЕННЫЕ ОТНОШЕНИЯ Тексты лекций для студентов экономических специальностей очной и заочной формы обучения Минск 2010 УДК 339.543(042.4) ББК 65.5я73 М36 Рассмотрены и рекомендованы к изданию редакционноиздательским советом университета. Рецензенты: доктор экономических наук, профессор, декан факультета Международных экономических отношений УО Белорусский государственный экономический университет Г....»

«ЮГО-ЗАПАДНОЕ ОКРУЖНОЕ УПРАВЛЕНИЕ ОБРАЗОВАНИЯ ДЕПАРТАМЕНТА ОБРАЗОВАНИЯ ГОРОДА МОСКВЫ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ ОБРАЗОВАТЕЛЬНОЕ УЧРЕЖДЕНИЕ ГОРОДА МОСКВЫ СРЕДНЯЯ ОБЩЕОБРАЗОВАТЕЛЬНАЯ ШКОЛА С УГЛУБЛЕННЫМ ИЗУЧЕНИЕМ ОБЛАСТИ ЗНАНИЙ ИСКУССТВО № 1372 Рабочая программа по технологии 1 класс Б УМК Школа России Составила: Шарабурова И.В. 2013-2014 учебный год Москва 2013 г. Пояснительная записка Программа разработана на основе Федерального государственного образовательного стандарта начального общего...»

«1 Паспорт.. стр 4-6 Введение..стр. 7-8 Общая характеристика социума села, школы..стр.8-9 Общая информация об общеобразовательном учреждении. стр. 10 Социальный паспорт школы.. стр. 11 Сведения об обучающихся.. стр.11 Контингент выпускников по годам и ступеням обучения. Контингент выпускников, поступивших в различные учебные заведения. Качественная характеристика педагогического коллектива.стр. 13-14 Условия осуществления образовательного процесса.стр.15-17 Материально-техническая база...»

«МИНИСТЕРСТВО ОБРАЗОВАНИЯ И НАУКИ РОССИЙСКОЙ ФЕДЕРАЦИИ Федеральное государственное бюджетное образовательное учреждение высшего профессионального образования Тихоокеанский государственный университет ПРИНЯТО Ученым Советом Тихоокеанского государственного университета Протокол № 16 от 18 мая 2012г. Председатель Ученого Совета / С.Н.Иванченко ПРОГРАММА вступительного экзамена по научной специальности 05.21.01 Технология и машины лесозаготовок и лесного хозяйства (технические науки) Хабаровск 2012...»

«Рабочая программа учебной дисФ ТПУ 7.1 -21/01 циплины ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ОБРАЗОВАНИЮ Государственное образовательное учреждение высшего профессионального образования Томский политехнический университет УТВЕРЖДАЮ: Декан факультета ГФ _В.Г. РУБАНОВ Мировая культура и искусство Рабочая программа для специальности 230500 – Социально-культурный сервис и туризм Факультет: Гуманитарный (ГФ) Обеспечивающая кафедра Культурологии и социальной коммуникации Курс 1, Семестр 2- Распределение учебного...»






 
© 2013 www.diss.seluk.ru - «Бесплатная электронная библиотека - Авторефераты, Диссертации, Монографии, Методички, учебные программы»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.