Меню
Публикации
2024
2023
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
2008
2007
2006
2005
2004
2003
2002
2001
Главный редактор
НИКИФОРОВ
Владимир Олегович
д.т.н., профессор
Партнеры
Аннотации номера
ВВЕДЕНИЕ В АВТОМАТНОЕ ПРОГРАММИРОВАНИЕ
ПАРАДИГМА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
Шалыто А. А.
3
В статье приводятся основные положения автоматного программирования и обосновываются преимущества его использования при разработке программного обеспечения. Описываются инструментальные средства для поддержки автоматного программирования и приводятся примеры успешного применения предлагаемого подхода на практике. В статье описывается процедурное программирование с явным выделением состояний и объектно-ориентированное программирование с явным выделением состояний. Автоматные программы могут быть эффективно верифицированы, а для их построения в ряде случаев могут быть применены генетические алгоритмы.
ПОСТРОЕНИЕ АВТОМАТОВ ДЛЯ УПРАВЛЕНИЯ БЕСПИЛОТНЫМИ УСТРОЙСТВАМИ НА ОСНОВЕ ПРИМЕНЕНИЯ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ С БОЛЬШИМ ЧИСЛОМ ВХОДНЫХ ПЕРЕМЕННЫХ
Поликарпова Н. И., Точилин В. ., Шалыто А. А.
24
Эффективность известных методов автоматической генерации конечных автоматов на основе генетического программирования экспоненциально снижается с ростом числа входных воздействий автомата. В работе предложен метод, который не имеет указанного недостатка. Предпочтительность применения предложенного метода при большом числе входных воздействий обоснована теоретически. Метод был применен в инструментальном средстве для автоматизации разработки системы управления самолетом на высоком уровне абстракции.
42
В работе рассматривается применение генетических алгоритмов для построения системы управления беспилотным летательным аппаратом. Система управления строится как совокупность искусственной нейронной сети и конечного автомата. Нейронная сеть преобразует входные вещественные переменные в логические, которые подаются на вход конечному автомату. Он, в свою очередь, вырабатывает выходные воздействия. Для оптимизации этой модели используется генетическое программирование.
ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКОГО ПРОГРАММИРОВАНИЯ И МЕТОДОВ СОКРАЩЕННЫХ ТАБЛИЦ ПЕРЕХОДОВ
И ДЕРЕВЬЕВ РЕШЕНИЙ ДЛЯ ПОСТРОЕНИЯ АВТОМАТОВ УПРАВЛЕНИЯ МОДЕЛЬЮ БЕСПИЛОТНОГО ЛЕТАТЕЛЬНОГО АППАРАТА
Соколов Д. О., Царев Ф. Н., Давыдов А. .
60
В работе рассматривается применение генетического программирования для построения конечных автоматов, управляющих системами со сложным поведением. Для представления конечных автоматов используются два метода: метод сокращенных таблиц переходов и метод представления автоматов деревьями решений. Применение этих методов иллюстрируется на примере задачи об управлении моделью беспилотного летательного аппарата.
ПОСТРОЕНИЕ АВТОПИЛОТА ДЛЯ УПРОЩЕННОЙ МОДЕЛИ ВЕРТОЛЕТА С ПОМОЩЬЮ ГЕНЕТИЧЕСКОГО АЛГОРИТМА
Лобанов П. Г., Сытник С. А., Шалыто А. А.
79
Предложен генетический алгоритм построения автопилота для упрощенной модели вертолета. Задачей вертолета является прохождение заданного множества целей в заданном порядке. алгоритм реализован на языке программирования Java. Выполнены вычислительные эксперименты, демонстрирующие эффективность этого алгоритма.
СОЗДАНИЕ СИСТЕМЫ УПРАВЛЕНИЯ ТАНКОМ ДЛЯ ИГРЫ ROBOCODE С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ
АЛГОРИТМОВ
Бедный Ю. ., Шалыто А. А.
88
В работе предлагается метод создания системы управления танком для игры Robocode, основанный на применении генетических алгоритмов, что позволяет автоматизировать процесс построения системы управления. Кроме того, рассматривается способ улучшения генерируемых систем управления за счет использования более сложного алгоритма управления, реализованного с помощью конечного автомата.
ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ
РАЗРАБОТКА ИНСТРУМЕНТАЛЬНОГО СРЕДСТВА ДЛЯ ГЕНЕРАЦИИ КОНЕЧНЫХ АВТОМАТОВ С ИСПОЛЬЗОВАНИЕМ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ
Мандриков Е. ., Кулев В. А.
100
В рамках проведения научно-исследовательской работы выполняется разработка инструментального средства для генерации автоматов на основе генетического программирования, которое позволяет повысить уровень автоматизации проектирования автоматных программ. На английском языке это инструментальное средство имеет аббревиатуру – GAAP (Genetic Algorithms for Automata-based Programming).
103
В работе предлагается новый метод представления автоматов в виде особей эволюционного алгоритма, основанный на деревьях решений. Предлагаемый метод представления автоматов позволяет существенно сократить объем требуемой для работы эволюционного алгоритма памяти. Разработан метод генетического программирования, основанный на предложенном представлении. Эффективность разработанного метода демонстрируется на примере решения одного из вариантов задачи об «Умном муравье».
ПРИМЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ПОСТРОЕНИЯ
АВТОМАТОВ МУРА И СИСТЕМ ВЗАИМОДЕЙСТВУЮЩИХ АВТОМАТОВ МИЛИ НА ПРИМЕРЕ ЗАДАЧИ ОБ «УМНОМ МУРАВЬЕ»
Соколов Д. О., Царев Ф. Н., Давыдов А. .
108
В работе предлагается генетический алгоритм, осуществляющий построение конечных автоматов Мура. Аналогичный алгоритм предлагается применять и для построения систем взаимодействующих автоматов Мили. Для указанных типов автоматов разработаны генетические операции скрещивания и мутации. Реализация генетических алгоритмов выполнена на языке программирования Java. Применение этих алгоритмов иллюстрируется на примере задачи об «Умном муравье».
114
Предложены три метода, позволяющие повысить скорость сходимости стандартных генетических алгоритмов для класса задач, в которых решением является конечный автомат. Первый из этих методов позволяет сократить число состояний автомата за счет использования флагов. Метод восстановления связей между состояниями позволяет сократить число неиспользуемых состояний автомата. Метод сортировки состояний в порядке использования позволяет уменьшить число состояний автомата.
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ
МЕТОДЫ ВЕРИФИКАЦИИ МОДЕЛЕЙ АВТОМАТНЫХ ПРОГРАММ
Вельдер С. Э., Шалыто А. А.
123
В статье рассматриваются способы преобразования программ, разработанных на основе автоматного подхода, в модели Крипке, предназначенные для проверки свойств, относящихся к поведению системы. Эти свойства задаются формулами темпоральной логики. Предложены несколько методов такого преобразования и способов формулировки свойств.
ВЕРИФИКАЦИЯ ПРОГРАММ, ПОСТРОЕННЫХ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА С ИСПОЛЬЗОВАНИЕМ ПРОГРАММНОГО СРЕДСТВА SMV
Курбацкий Е. .
137
В работе рассматривается метод верификации программ, построенных на основе автоматного подхода c использованием метода проверки на моделях (Model Checking). Для проверки модели используется программное средство SMV. При предлагаемом подходе система переходов не строится в явном виде, что позволяет верифицировать программы с большим числом состояний.
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ С ИСПОЛЬЗОВАНИЕМ ВЕРИФИКАТОРА SPIN
Шалыто А. А., Лукин М. А.
145
Рассматривается способ использования верификатора SPIN для верификации автоматных программ. При использовании этого верификатора модель описывается на языке Promela, а требования – на языке LTL. В работе предлагается метод автоматизированного преобразования автоматных программ в модели на языке Promela. Для преобразования формулы на языке LTL в вид, пригодный для использования верификатором, разработано специальное программное средство. Использование предлагаемого метода иллюстрируется на примере верификации модели банкомата.
ВЕРИФИКАЦИЯ АВТОМАТНЫХ ПРОГРАММ ПРИ ПОМОЩИ ВЕРИФИКАТОРА UNIMOD.VERIFIER
Гуров В. С., Яминов Б. .
162
Описан разработанный авторами верификатор автоматных программ, созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. Верификатор работает за счет интеграции инструментального средства UniMod и верификатора программ Bogor. При использовании разработанного верификатора отсутствует необходимость преобразовывать автоматную программу во входной язык верификатора. Требования к программе записываются на языке темпоральной логики LTL.
РАЗРАБОТКА ВЕРИФИКАТОРА АВТОМАТНЫХ ПРОГРАММ
Егоров К. В., Шалыто А. А.
177
В статье описан разработанный авторами верификатор автоматных программ, созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. При его использовании, в отличие от известных верификаторов, отсутствует необходимость описывать модель на входном языке верификатора. Требования к программе записываются на языке темпоральной логики линейного времени LTL (Linear Time Logic). При использовании такой логики верификация осуществляется за счет пересечения автомата-произведения модели и автомата Бюхи, построенного для отрицания LTL-формулы.
189
В статье предлагается подход, повышающий надежность процесса разработки Java Card-апплетов. Формулируются особенности проектирования апплетов при применении автоматного подхода, предлагается расширенная утверждениями модель для описания функциональности, генератор кода с заглушками и инструмент для автоматизации тестирования полученных апплетов.
РАЗРАБОТКА КОРРЕКТНЫХ JAVA CARD-ПРОГРАММ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
Клебанов А. А., Шалыто А. А.
198
В данной работе описываются результаты исследований, направленных на создание корректного Java Card-кода. При этом код генерируется из высокоуровневого описания на основе технологии автоматного программирования. Дополнительным достоинством подобного подхода является возможность генерации формальной спецификации приложения. Соответствие исходного или byte-кода спецификации может быть проверено различными верификаторами или средствами динамической или статической проверки.
ВЕРИФИКАЦИИ ВЗАИМОДЕЙСТВИЯ ЧАСТЕЙ РЕАКТИВНОЙ СИСТЕМЫ, РЕАЛИЗОВАННЫХ С ПОМОЩЬЮ АВТОМАТНОГО
ПОДХОДА
Канжелев С. .
211
В работе рассматриваются вопросы верификации частей реактивной системы, каждая из которых реализована с помощью автоматного подхода. Рассматриваются проблемы, которые могут возникать в таких системах, а также спопобы их обнаружения для различных видов их семантической интерпретации.
221
В настоящей работе предлагается метод автоматической динамической верификации систем автоматов Мили, основанный на обходе альтернирующих автоматов. Описывается структура метода, правила построения протоколов и спецификации, а также выполняется анализ функциональных характеристик метода на основе разработанной реализации.
МЕТОДЫ РАЗРАБОТКИ АВТОМАТНЫХ ПРОГРАММ
ДЕКЛАРАТИВНЫЙ ПОДХОД К ВЛОЖЕНИЮ И НАСЛЕДОВАНИЮ АВТОМАТНЫХ КЛАССОВ ПРИ ИСПОЛЬЗОВАНИИ ИМПЕРАТИВНЫХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ
Астафуров А. .
230
В работе предлагается декларативный подход к реализации автоматных объектов при использовании объектно-ориентированных императивных языков программирования со статической проверкой типов. Отличительной особенностью предлагаемого подхода является возможность применения наследования и вложения макросостояний.
НАСЛЕДОВАНИЕ АВТОМАТНЫХ КЛАССОВ С ИСПОЛЬЗОВАНИЕМ ДИНАМИЧЕСКИХ ЯЗЫКОВ ПРОГРАММИРОВАНИЯ НА ПРИМЕРЕ RUBY
Тимофеев К. ., Астафуров А. .
238
Объектно-ориентированное программирование с явным выделением состояний совмещает в себе основные преимущества объектно-ориентированной и автоматной парадигм программирования. Основными достоинствами такого подхода являются расширяемость, гибкость и наличие механизма описания сложного поведения, реализованного на конечных автоматах. В данной работе рассматриваются объектноориентированный и динамический подходы к наследованию и вложению автоматных классов с использованием динамических языков программирования.
ИНСТРУМЕНТАЛЬНЫЕ СРЕДСТВА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
ИНСТРУМЕНТАЛЬНОЕ СРЕДСТВО ДЛЯ ПОДДЕРЖКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ UNIMOD 2. ПРОЕКТИРОВАНИЕ. ВАЛИДАЦИЯ. ВЕРИФИКАЦИЯ. РЕАЛИЗАЦИЯ
Кочелаев Д. ., Лагунов И. ., Хасянзянов Б. ., Яминов Б. .
251
В данной статье дается краткий обзор инструментального средства UniMod 2 для поддержки автоматного программирования. Данное инструментальное средство предназначено для разработки автоматных программ и предоставляет средства для визуального проектирования, отладки, валидации и верификации автоматных программ.
ТЕКСТОВЫЕ ЯЗЫКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ
Гуров В. С., Мазин М. А., Шалыто А. А.
258
В настоящей работе описывается текстовый язык автоматного программирования, построенный на основе системы метапрограммирования JetBrains MetaProgramming System (MPS). Этот язык лишен таких недостатков графического языка автоматного программирования, как низкая скорость ввода диаграмм, и более привычен для программиста.
263
Инструментальное средство UniMod позволяет проектировать и исполнять автоматные программы. Основное его ограничение – возможность только визуального описания конечных автоматов. В статье рассматриваются текстовый язык автоматного программирования FSML (Finite State Machine Language) и его редактор, позволяющие описывать автоматы в указанном средстве с помощью текстового языка автоматного программирования.
ТЕСТИРОВАНИЕ ПРИЛОЖЕНИЙ И КОНЕЧНЫЕ АВТОМАТЫ
МЕТОД РАЗРАБОТКИ ТЕСТОВ ДЛЯ ПРОГРАММНЫХ ИНТЕРФЕЙСОВ ПРИЛОЖЕНИЙ НА ОСНОВЕ КОНЕЧНО-АВТОМАТНОЙ МОДЕЛИ ТЕСТИРОВАНИЯ
Рубинов К. В., Веденеев В. ., Парфенов В. Г.
273
В работе описывается предложенный авторами метод разработки тестов для программных интерфейсов приложений на основе конечно-автоматной модели тестирования. Предлагаемый метод предполагает построение автоматной модели тестирования в графическом виде. После этого по этой модели с помощью обхода графа переходов строится набор тестовых сценариев. Такой подход к тестированию позволяет упростить и формализовать построение тестов не только для отдельных функций, но и для их совокупностей.
АВТОМАТНОЕ ПРОГРАММИРОВАНИЕ МОБИЛЬНЫХ РОБОТОВ
ПОСТРОЕНИЕ СИСТЕМЫ АВТОМАТИЧЕСКОГО УПРАВЛЕНИЯ МОБИЛЬНЫМ РОБОТОМ НА ОСНОВЕ АВТОМАТНОГО ПОДХОДА
Клебан В. О., Парфенов В. Г., Шалыто А. А.
281
В настоящей работе описывается подход к созданию системы автоматического управления мобильным роботом на основе автоматного подхода. Автоматное программирование применяется для написания программного обеспечения робота КВАРК-М на всех трех уровнях: на верхнем уровне применяется три автомата, на среднем – пять, а на нижнем – одиннадцать. Такой подход позволяет существенно повысить качество программного обеспечения роботов.
ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ
ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ
Клебан В. О., Новиков Ф. .
286
В работе рассматривается задача построения системы автоматизации документооборота. Для построения системы автоматизации документооборота применяются конечные автоматы, так как такой подход имеет ряд преимуществ по сравнению с традиционным. В качестве примера применения предлагаемого подхода рассматривается построение инструментального программного средства на базе Microsoft Office, которое предназначено для разработки и внедрения автоматизированной системы менеджмента качества в компаниях с проектным типом организации производства.
ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ И КОНЕЧНЫЕ АВТОМАТЫ
295
В работе предлагается метод, упрощающий процесс обучения класса сложных систем с большим числом входных данных и выходных воздействий. Он позволяет учитывать ограничения на поведение системы, что ведет к уменьшению размерности пространства поиска решений, удобным образом организовать разбиение задач системы на подзадачи, выполнению каждой из которых можно обучать систему отдельно от других и на основе различных методов машинного обучения. После этого полученные решения могут быть объединены с обеспечением достаточно сложные условия перехода между выполнением подзадач, в том числе вероятностные.