Аннотации номера

ВВЕДЕНИЕ В АВТОМАТНОЕ ПРОГРАММИРОВАНИЕ

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

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

24
Эффективность известных методов автоматической генерации конечных автоматов на основе генетического программирования экспоненциально снижается с ростом числа входных воздействий автомата. В работе предложен метод,  который не имеет указанного недостатка.  Предпочтительность применения предложенного метода при большом числе входных воздействий обоснована теоретически. Метод был применен в инструментальном средстве для автоматизации разработки системы управления самолетом на высоком уровне абстракции.
42
В работе рассматривается применение генетических алгоритмов для построения системы управления беспилотным летательным аппаратом.  Система управления строится как совокупность искусственной нейронной сети и конечного автомата. Нейронная сеть преобразует входные вещественные переменные в логические, которые подаются на вход конечному автомату. Он, в свою очередь, вырабатывает выходные воздействия. Для оптимизации этой модели используется генетическое программирование.
60
В работе рассматривается применение генетического программирования для построения конечных автоматов,  управляющих системами со сложным поведением. Для представления конечных автоматов используются два метода: метод сокращенных таблиц переходов и метод представления автоматов деревьями решений.  Применение этих методов иллюстрируется на примере задачи об управлении моделью беспилотного летательного аппарата.  
79
Предложен генетический алгоритм построения автопилота для упрощенной модели вертолета. Задачей вертолета является прохождение заданного множества целей в заданном порядке. алгоритм реализован на языке программирования Java.  Выполнены вычислительные эксперименты,  демонстрирующие эффективность этого алгоритма.
88
В работе предлагается метод создания системы управления танком для игры Robocode, основанный на применении генетических алгоритмов,  что позволяет автоматизировать процесс построения системы управления. Кроме того,  рассматривается способ улучшения генерируемых систем управления за счет использования более сложного алгоритма управления, реализованного с помощью конечного автомата.

ПРИМЕНЕНИЕ ГЕНЕТИЧЕСКИХ АЛГОРИТМОВ ДЛЯ ГЕНЕРАЦИИ АВТОМАТОВ

100
В рамках проведения научно-исследовательской работы выполняется разработка инструментального средства для генерации автоматов на основе генетического программирования, которое позволяет повысить уровень автоматизации проектирования автоматных программ.  На английском языке это инструментальное средство имеет аббревиатуру – GAAP (Genetic Algorithms for Automata-based Programming).
103
В работе предлагается новый метод представления автоматов в виде особей эволюционного алгоритма, основанный на деревьях решений. Предлагаемый метод представления автоматов позволяет существенно сократить объем требуемой для работы эволюционного алгоритма памяти. Разработан метод генетического программирования, основанный на предложенном представлении. Эффективность разработанного метода демонстрируется на примере решения одного из вариантов задачи об «Умном муравье». 
108
В работе предлагается генетический алгоритм, осуществляющий построение конечных автоматов Мура. Аналогичный алгоритм предлагается применять и для построения систем взаимодействующих автоматов Мили.  Для указанных типов автоматов разработаны генетические операции скрещивания и мутации. Реализация генетических алгоритмов выполнена на языке программирования Java.  Применение этих алгоритмов иллюстрируется на примере задачи об «Умном муравье».
114
Предложены три метода, позволяющие повысить скорость сходимости стандартных генетических алгоритмов для класса задач, в которых решением является конечный автомат. Первый из этих методов позволяет сократить число состояний автомата за счет использования флагов. Метод восстановления связей между состояниями позволяет сократить число неиспользуемых состояний автомата. Метод сортировки состояний в порядке использования позволяет уменьшить число состояний автомата.

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

123
В статье рассматриваются способы преобразования программ,  разработанных на основе автоматного подхода, в модели Крипке, предназначенные для проверки свойств, относящихся к поведению системы. Эти свойства задаются формулами темпоральной логики. Предложены несколько методов такого преобразования и способов формулировки свойств.
137
В работе рассматривается метод верификации программ, построенных на основе автоматного подхода c использованием метода проверки на моделях (Model Checking). Для проверки модели используется программное средство SMV. При предлагаемом подходе система переходов не строится в явном виде, что позволяет верифицировать программы с большим числом состояний.
145
Рассматривается способ использования верификатора SPIN для верификации автоматных программ. При использовании этого верификатора модель описывается на языке Promela, а требования – на языке LTL. В работе предлагается метод автоматизированного преобразования автоматных программ в модели на языке Promela. Для преобразования формулы на языке LTL в вид, пригодный для использования верификатором, разработано специальное программное средство. Использование предлагаемого метода иллюстрируется на примере верификации модели банкомата.
162
Описан разработанный авторами верификатор автоматных программ,  созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. Верификатор работает за счет интеграции инструментального средства UniMod и верификатора программ Bogor. При использовании разработанного верификатора отсутствует необходимость преобразовывать автоматную программу во входной язык верификатора. Требования к программе записываются на языке темпоральной логики LTL.
177
В статье описан разработанный авторами верификатор автоматных программ,  созданных при помощи инструментального средства для поддержки автоматного программирования UniMod. При его использовании, в отличие от известных верификаторов, отсутствует необходимость описывать модель на входном языке верификатора. Требования к программе записываются на языке темпоральной логики линейного времени LTL (Linear Time Logic). При использовании такой логики верификация осуществляется за счет пересечения автомата-произведения модели и автомата Бюхи, построенного для отрицания LTL-формулы.
189
В статье предлагается подход, повышающий надежность процесса разработки Java Card-апплетов. Формулируются особенности проектирования апплетов при применении автоматного подхода,  предлагается расширенная утверждениями модель для описания функциональности,  генератор кода с заглушками и инструмент для автоматизации тестирования полученных апплетов.
198
В данной работе описываются результаты исследований,  направленных на создание корректного Java Card-кода. При этом код генерируется из высокоуровневого описания на основе технологии автоматного программирования. Дополнительным достоинством подобного подхода является возможность генерации формальной спецификации приложения.  Соответствие исходного или byte-кода спецификации может быть проверено различными верификаторами или средствами динамической или статической проверки.
211
В работе рассматриваются вопросы верификации частей реактивной системы, каждая из которых реализована с помощью автоматного подхода. Рассматриваются проблемы, которые могут возникать в таких системах, а также спопобы их обнаружения для различных видов их семантической интерпретации.
221
В настоящей работе предлагается метод автоматической динамической верификации систем автоматов Мили, основанный на обходе альтернирующих автоматов. Описывается структура метода, правила построения протоколов и спецификации, а также выполняется анализ функциональных характеристик метода на основе разработанной реализации.

МЕТОДЫ РАЗРАБОТКИ АВТОМАТНЫХ ПРОГРАММ

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

ИНСТРУМЕНТАЛЬНЫЕ СРЕДСТВА АВТОМАТНОГО ПРОГРАММИРОВАНИЯ

251
В данной статье дается краткий обзор инструментального средства UniMod 2 для поддержки автоматного программирования. Данное инструментальное средство предназначено для разработки автоматных программ и предоставляет средства для визуального проектирования,  отладки,  валидации и верификации автоматных программ.

ТЕКСТОВЫЕ ЯЗЫКИ АВТОМАТНОГО ПРОГРАММИРОВАНИЯ

ТЕКСТОВЫЙ ЯЗЫК АВТОМАТНОГО ПРОГРАММИРОВАНИЯ Гуров В. С., Мазин М. А., Шалыто А. А.
258
В настоящей работе описывается текстовый язык автоматного программирования, построенный на основе системы метапрограммирования JetBrains MetaProgramming System (MPS).  Этот язык лишен таких недостатков графического языка автоматного программирования, как низкая скорость ввода диаграмм, и более привычен для программиста.
263
Инструментальное средство UniMod позволяет проектировать и исполнять автоматные программы. Основное его ограничение – возможность только визуального описания конечных автоматов. В статье рассматриваются текстовый язык автоматного программирования FSML  (Finite State Machine Language)  и его редактор, позволяющие описывать автоматы в указанном средстве с помощью текстового языка автоматного программирования.

ТЕСТИРОВАНИЕ ПРИЛОЖЕНИЙ И КОНЕЧНЫЕ АВТОМАТЫ

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

АВТОМАТНОЕ ПРОГРАММИРОВАНИЕ МОБИЛЬНЫХ РОБОТОВ

281
В настоящей работе описывается подход к созданию системы автоматического управления мобильным роботом на основе автоматного подхода. Автоматное программирование применяется для написания программного обеспечения робота КВАРК-М на всех трех уровнях: на верхнем уровне применяется три автомата, на среднем – пять, а на нижнем – одиннадцать. Такой подход позволяет существенно повысить качество программного обеспечения роботов.

ПРИМЕНЕНИЕ КОНЕЧНЫХ АВТОМАТОВ В ДОКУМЕНТООБОРОТЕ

286
В работе рассматривается задача построения системы автоматизации документооборота. Для построения системы автоматизации документооборота применяются конечные автоматы, так как такой подход имеет ряд преимуществ по сравнению с традиционным. В качестве примера применения предлагаемого подхода рассматривается построение инструментального программного средства на базе Microsoft Office, которое предназначено для разработки и внедрения автоматизированной системы менеджмента качества в компаниях с проектным типом организации производства.

ИСКУССТВЕННЫЙ ИНТЕЛЛЕКТ И КОНЕЧНЫЕ АВТОМАТЫ

295
В работе предлагается метод, упрощающий процесс обучения класса сложных систем с большим числом входных данных и выходных воздействий. Он позволяет учитывать ограничения на поведение системы, что ведет к уменьшению размерности пространства поиска решений,  удобным образом организовать разбиение задач системы на подзадачи, выполнению каждой из которых можно обучать систему отдельно от других и на основе различных методов машинного обучения. После этого полученные решения могут быть объединены с обеспечением достаточно сложные условия перехода между выполнением подзадач, в том числе вероятностные.
Информация 2001-2019 ©
Научно-технический вестник информационных технологий, механики и оптики.
Все права защищены.

Яндекс.Метрика