17.05.2022

О развитии автоматного программирования:
отклик А. Шалыто на серию вебинаров ИСИС

Институт автоматики и электрометрии СО РАН и Институт систем информатики СО РАН им. А.П. Ершова проводят межинститутский семинар «Инжиниринг современных информационных систем» (https://www.iae.nsk.su/ru/seminars-and-conferences/sem-isis). Руководитель семинара – докт. техн. наук ­Владимир Евгеньевич Зюбин (https://www.iae.nsk.su/ru/laboratory-sites/lab-19, Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.).

15.03.2019 г. Владимир Иванович Шелехов (Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.) из Института систем информатики сделал на этом семинаре доклад на тему: «Язык требований в автоматном программировании» (https://www.youtube.com/watch?v=IpZ9VlIcHYQ&t=45s).

В начале докладчик рассказал о «первой производной» его исследований в области программирования – предикатном программировании (https://persons.iis.nsk.su/files/persons/pages/predbase.pdf).

Оно появилось как отрицание теории схем-программ, структурного программирования (избавление от оператора go to не привело к существенному улучшению процесса программирования) и императивного программирования (https://ru.wikipedia.org/wiki/Императивное_программирование). Функциональное программирование не заменяет императивное программирование, и это причина появления предикатного программирования. Однако в рамках последнего не все программы реализуются, так как оно ограничено классом программ-функций. Программа принадлежит классу программ-функций, если она не взаимодействует с внешним окружением. Точнее, если возможно перестроить программу таким образом, чтобы все операторы ввода данных находились в начале программы, а весь вывод собран в ее конце. Класс программ-функций, по меньшей мере, содержит программы для задач дискретной и вычислительной математики.

Если подобная перестройка программы принципиально невозможна, ее следует определять как программу-процесс (реактивную систему), для которой характерно аппаратно-программное окружение. К реактивным относятся системы управления. Для реализации программ-процессов предназначено автоматное программирование.

Указанные классы составляют более 90% всех программ. Имеются другие более сложные типы программ, например, языковые процессоры и операционные системы.

В начале двухтысячных автоматное программирование стало для Шелехова «второй производной» его исследований.

Я стал публиковаться по этой тематике на виду несколько раньше. Моя книга о Switch-технологии (http://is.ifmo.ru/books/switch/1) появилась в 1998 г., а в аннотации к моей статье: Автоматное проектирование программ. Алгоритмизация и программирование задач логического управления // Известия РАН. Теория и системы управления. 2000. № 6, с. 63-81 (https://www.avrorasystems.com/ru/Data/Pressroom/Files/ran.pdf) было сказано: «Описываемая технология может быть названа автоматной технологией, а соответствующая область программирования – автоматным программированием». Этот термин был предложен Дмитрием Александровичем Поспеловым, когда я рассказывал ему про этот подход в 1997 г. (//vk.com/@1077823-vtomatnoe-programmirovanie">https://vk.com/@1077823-vtomatnoe-programmirovanie).

Как, по мнению Шелехова, строится автоматное программирование (засечка 19.48)?

I. Автоматное программирование по Шалыто базируется на императивном программировании (языки Java, C, С++).

II. Автоматное программирование может быть основано функциональном программировании (язык Erlang, в котором в явном виде нет состояний, что приводит к тяжелому и противоестественному программированию, и язык «Рефлекс», http://reflex-language.narod.ru/).

Мы пробовали этот вариант автоматного программирования, непосредственно используя функциональные языки программирования: 1. Малаховски Я.М., Шалыто А.А. Конечные автоматы в чистых функциональных языках программирования. Автоматы и Haskell // RSDN Magazine 2009. № 3, с. 20-26. https://rsdn.org/article/haskell/HaskellStateMachine.xml. 2. Малаховски Я.М., Шалыто А.А. Реализация конечных автоматов на функциональных языках программирования // Информационно-управляющие системы. 2009. № 6, с. 30-33. http://www.i-us.ru/index.php/ius/article/view/14898). 3. Малаховски Я.М., Корнеев Г.А. Валидация автоматов с переменными на функциональных языках программирования // Научно-технический вестник Санкт-Петербургского государственного университета информационных технологий, механики и оптики. 2010. № 6, с. 73-77. https://ntv.ifmo.ru/file/article/404.pdf. 4. Малаховски Я.М., Шалыто А.А. Библиотека поддержки автоматного программирования для языка Haskell // Свидетельство о государственной регистрации программы для ЭВМ. № 2010 614196. Дата регистрации ­– 29.06.2010. 5. Малаховски Я.М. Применение систем типов для валидации и верификации автоматных программ / Сборник «СПИСОК-2011». Материалы второй межвузовской научной конференции по проблемам информатики». СПб.: ВВМ. 2011, с. 368, 369. http://is.ifmo.ru/works/2011/SPISOK/13-Malahovski.pdf. Не мы, не докладчик это направление не развивали.

III. Шелехов, который не признает структурное программирование и использует операторы перехода, строит автоматное программирование на базе предикатного программирования. При этом «третьей производной» его исследований стал язык автоматного программирования. Перед ним встал вопрос: «Что такое спецификация автоматных программ?». Он пытался использовать теории процессов Хоара и Милнера. Оказалось, что для применения в технологии эти теории – тупик. Докладчик сказал, что попадал и в другие тупики. История науки – преодоление тупиков. ­Шелехов пришел к выводу: спецификация автоматных программ – требования к ним. Спецификация в виде требований переписывается в автоматную программу. Тем самым язык требований может быть использован в качестве языка автоматных программ.

При этом отмечу, что если в моем подходе спецификация – система графов переходов, то у Шелехова – это текст на языке требований, на котором, по словам автора, автоматная программа не всегда получается корректной, что требует трансформации требований – добавления новых ограничений, например, использующих темпоральную логику. Я считаю, что здесь в «полный рост» имеет место эвристика, а когда автор говорит, что его подход упрощает процесс построения программ, то это не очевидно.

Поясняя свой подход, Владимир Иванович говорит: «Картинка здесь тоже понятная», но картинок у него нет – только тексты на предложенном языке требований. При этом автоматная программа пишется, как говорит Шелехов, «в стиле языка «Фортран» и представляется в виде набора правил: управляющее состояние М: <условие 1>, … <условие n> стрелка <действие 1>, … <действие m> #управляющее состояние L. Правила выполняются последовательно.

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

Еще один доклад на том же семинаре Шелехов сделал 01.04.2022 г. Его тема: «Автоматное программирование на базе системы моделирования и верификации Event-B» (https://www.youtube.com/watch?v=la-DLQ4uf8M).

На первом слайде докладчик изложил, как, по его мнению, формировался понятийный базис программирования: «Становление теории программирования: 1. Языки программирования. Синтаксис. Семантика. 2. Трансляторы. Операционные системы. Базы данных. 3. Структурное программирование. 4. Технологии программирования. 5. Абстрактные типы данных. 6. Объектно-ориентированное программирование. 7. Понятие спецификации. Предусловие. Постусловие. 8. Реактивные системы. Автоматные методы. 9. Автоматное программирование. 10. Формальные методы.

На засечке 1.44 Владимир Иванович говорит: «Термины «Реактивные системы» и «Автоматные методы» появились в девяностые годы. Чуть позже возникло «автоматное программирование», причем появилось только у нас по инициативе Шалыто. Им было введено понятие «управляющее состояние». Шелехов тоже использует это понятие в «своем» автоматном программировании. На засечке 8.28 снова появляется автоматное программирование по Шалыто. На засечке 19.53 Шелехов среди способов кодирования автоматных программ рассматривает предложенную мною Switch-технологию, в которой не используется оператор go to, что позволяет реализовывать автоматные программы на языке Java, в частности.

Шелехов и в этом докладе отметил, что для автоматных программ методы Хоара и Флойда непригодны для дедуктивной верификации (https://ru.wikipedia.org/wiki/Верификация, https://ru.wikipedia.org/wiki/Формальная_верификация). Он рассмотрел язык автоматного программирования, построенный расширением языка спецификаций Event-B (http://www.event-b.org/), возникшего на базе модификации метода B (https://en.wikipedia.org/wiki/B-Method), предназначенного для разработки программного обеспечения критически важных систем безопасности и, в первую очередь, для метро и железнодорожного транспорта. Шелехов определил модель Event-B (Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 2010. 586 p.) для автоматного программирования. Докладчик описал технологию разработки и верификации автоматных программ на базе системы Event-B. Эта технология была апробирована на примере большой задачи управления движением на мосту из руководства по системе Event-B.

Свободно распространяемая платформа Rodin, созданная трудом многих (в основном европейских) специалистов, является средой для разработки, анализа и верификации спецификаций при использовании метода Event-B. Платформа обеспечивает генерацию формул корректности инвариантов, поддерживает систему автоматического и интерактивного доказательства, содержит Model Checker, набор инструментов для доказательств, SMT-решатели (SMT-формула – это обобщение SAT-решателей, в которой переменные заменены предикатами из соответствующих теорий) и аниматор (https://www.ispras.ru/upload/iblock/5e5/5e5ac36633ead83d10476199d697be85.pdf).

Лекции и слайды к ним на русском языке по Event-B и Rodin приведены здесь: http://wasp.iis.nsk.su/page3.html.

По мнению докладчика, наличие таких мощных средств для рассматриваемого класса программ проведение верификации не гарантирует отсутствия ошибок (засечка 29.51).

К этому выводу мы пришли еще в 2013 г. Тогда я и Владимир Ульянцев написали статью «О верификации простых программ со сложным поведением» (http://is.ifmo.ru/works/2013/ulyantsev-shalyto-verification.pdf, //vk.com/@1077823-o-verifikacii-prostyh-programm-so-slozhnym-povedeniem" title="https://vk.com/@1077823-o-verifikacii-prostyh-programm-so-slozhnym-povedeniem">https://vk.com/@1077823-o-verifikacii-prostyh-programm-so-slozhnym-povedeniem), в которой показали, что качественно строить даже простые автоматные программы весьма сложно. О программах других классов и говорить не приходится.

Автоматное программирование излагается Шелеховым на двух лекциях в курсе «Формальные методы в программной инженерии» (http://wasp.iis.nsk.su), который преподается на механико-математическом факультете Новосибирского государственного университета. На первой из них (видео, http://wasp.iis.nsk.su/video/fap_lection1.mp4), слайды, http://wasp.iis.nsk.su/pres/fap_lecture1.pdf) Шелехов утверждает, что для систем реального времени нет единого подхода к их программной реализации. По его мнению, автоматное программирование в этой области играет особую роль. Он вновь подтвердил, что оно впервые было предложено в России, и его родоначальником был А. Шалыто, когда лет двадцать назад предложил технологию автоматного программирования, названную им «Switch-технология» (засечка 22.40).

В качестве одного из примеров создания автоматных программ (вторая лекция (http://wasp.iis.nsk.su/video/fap_lection2.mp4, http://wasp.iis.nsk.su/pres/fap_lecture2.pdf) целиком посвящена примерам построения автоматных программ на основе его подхода) Шелехов использует электронные часы с будильником (засечка 39.58) из моей с Н. Поликарповой книги «Автоматное программирование» (http://is.ifmo.ru/books/_book.pdf).

При этом он по словесному описанию строит автоматную программу в предлагаемом им стиле языка «Фортран», а потом для сравнения – на основе Switch-технологии, и делается вывод, что его программа более проста и понятна, а то, что моя программа построена формально и изоморфно по графу переходов, Шелехов не учитывает, так как графы переходов в качестве языка спецификации программ, в отличие от меня, он не использует.

При этом отмечу, что при применении программного средства Stateflow (https://www.mathworks.com/products/stateflow.html) графы переходов являются не только языком спецификации, но и языком программирования автоматных программ. Это позволяет генерировать их текстовое представление, которое может быть автоматически (без участия человека) загружено в среду исполнения. Видеоролик приведен ниже.

Публикации В.И. Шелехова:

1.Шелехов В.И. Язык и технология автоматного программирования // Программная инженерия. 2014. № 4, с. 3-15 (https://persons.iis.nsk.su/files/persons/pages/automatProg.pdf). В этой работе есть ссылки на две мои книги (http://is.ifmo.ru/books/switch/1, http://is.ifmo.ru/books/_book.pdf) и такой фрагмент: «Концепция автоматного программирования разработана Анатолием Шалыто, в том числе в интеграции с объектно-ориентированным программированием. Автоматная программа определяется как совокупность конечных автоматов. Используются графическое и текстовое представления программы. Управляющие состояния являются значениями переменной, соответствующей этим состояниям. При реализации автоматной программы применяется Switch-технология. Термин «автоматное программирование» и его аналог Automata-Based Programming применяется только в России. Тем не менее, автоматные методы программирования заложены во многих языках. Автор благодарен А.А. Шалыто за его работы по автоматному программированию. Предлагаемое мною понятие автоматной программы концептуально не отличается от введенного Анатолием Шалыто, однако различия в языке и технологии существенны».

2. Шелехов В.И. Разработка автоматных программ на базе определения требований // Системная информатика. 2014. № 4, c. 1-29 (http://persons.iis.nsk.su/files/persons/pages/req_tech.pdf. Есть ссылки на две указанные выше мои книги и на один наш курсовик, ссылка на который приведена ниже. Работа заканчивается так: «Автор благодарен А.А. Шалыто за работы по автоматному программированию, стимулировавшие мои исследования».

3. Шелехов В.И. Оптимизация автоматных программ методом трансформации требований // Программная инженерия. 2015. № 11, с. 3-13.
http://persons.iis.nsk.su/files/persons/pages/req_k.pdf. Наши работы не упоминаются.

4. Шелехов В.И. Классификация программ, ориентированная на технологию программирования // Программная инженерия. 2016. № 12. 2016, с. 531-538. https://persons.iis.nsk.su/files/persons/pages/prog.pdf. Автоматные программы в смтатье упоминаются, а мы – нет.

5. Шелехов В.И., Тумуров Э.Г. Технология автоматного программирования
на примере программы управления лифтом // Программная инженерия. 2017. № 3, с. 99-111 (https://persons.iis.nsk.su/files/persons/pages/lift1.pdf). В этой работе есть три ссылки на наши работы – на два курсовика наших студентов (Наумов А.С., Шалыто А.А. Система управления лифтом. 2003 (http://is.ifmo.ru/download/elevator_a.pdf), Решетников Е.О., Смачных М.В. Система управления пассажирским лифтом. 2006 (http://is.ifmo.ru/download/umlift.pdf) и мою книгу Switch-технология (http://is.ifmo.ru/books/switch/1), опубликованную почти двадцать лет до публикации этой статьи – в 1998 г. Интересно, что еще одну нашу работу про программирование лифта авторы статьи не заметили: Наумов Л.А., Шалыто А.А. Искусство программирования лифта. Объектно-ориентированное программирование с явным выделением состояний // Информационно-управляющие системы. 2003. № 6, с. 38-49. http://www.i-us.ru/index.php/ius/article/view/14406.

6. Шелехов В.И. Сравнение технологий автоматного программирования
и Event-B // Системная информатика. 2021. № 18, c. 53-84. https://system-informatics.ru/files/article/bridgesi.pdf. Имеется ссылка на мою книгу http://is.ifmo.ru/books/switch/1.

Платформу Rodin для верификации автоматных программ, специфицированных графами переходов, использует и специалист из Кургана Максим Нейзов (Этот адрес электронной почты защищён от спам-ботов. У вас должен быть включен JavaScript для просмотра.). 16 марта 2021 г. он на том же семинаре выступил с докладом на тему «Опыт верификации автоматных программ на платформе Rodin (на примере задачи управления генератором эндогаза)» (https://www.youtube.com/watch?v=Miqi4DWqS8o&t=303s).

Максим по этой теме опубликовал следующие работы:

1.Нейзов М. Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin. Часть 1. Определение требований надежности и безопасности работы генератора эндогаза // Современная электроника. 2020. № 9, с. 62, 63 (https://www.iae.nsk.su/images/stories/2_Science/5_Seminars-Conf/4_EngModernCompSys/210316-NeizovM/Neizov_part1.pdf). Формальный дедуктивный анализ представляет собой строгий математический подход к верификации алгоритмов: алгоритм описывается с помощью аксиом, а требуемые свойства доказываются как теоремы. Цель представленного анализа – доказать соответствие алгоритма управления предъявляемым требованиям надежности и безопасности. В статье описывается технологический процесс генерации эндогаза и определяются предъявляемые к нему требования надежности и безопасности.

2. Нейзов М. Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin. Часть 2. Алгоритм управления и платформа Rodin // Современная электроника. 2021. № 1, с. 44-47 (https://www.iae.nsk.su/images/stories/2_Science/5_Seminars-Conf/4_EngModernCompSys/210316-NeizovM/Neizov_part2.pdf). В статье представлен алгоритм управления в виде системы взаимосвязанных автоматов, заданных некоторой разновидностью графов переходов, и платформа Rodin – инструмент для формального анализа систем и автоматизации доказательства теорем. В этой части статьи есть ссылки на три наши работы. В работе используются и предложенные мною схемы связей автоматов с их окружением.

3. Нейзов М. Формальный дедуктивный анализ автоматного алгоритма управления генератором эндогаза с помощью платформы Rodin. Часть 3. Построение формальной теории для алгоритма управления // Современная электроника. 2021. № 2, с. 40-43 (https://www.iae.nsk.su/images/stories/2_Science/5_Seminars-Conf/4_EngModernCompSys/210316-NeizovM/Neizov_part3.pdf). В статье выполнено построение формальной теории для рассматриваемого алгоритма управления: проведена аксиоматизация алгоритма, формализованы требования, продемонстрировано доказательство теорем с помощью платформы Rodin.

11 ноября 2021 г. Максим выступал там же с докладом на тему «Автоматно-функциональная парадигма программирования реактивных систем» (https://www.youtube.com/watch?v=iyw98xpsJgw), где он попытался недостатки автоматной парадигмы заменить достоинствами функциональной парадигмы и наоборот.

Шестого мая 2022 г. Нейзов сделал доклад на тему «Автоматно-функциональный подход к моделированию киберфизических систем (на примере Event-B модели для верификации свойств алгоритма управления движением автомобилей на мосту)», в котором рассказал как с помощью его подхода строить модели для указанного класса систем корректных алгоритмов управления методом доказательства теорем (https://www.youtube.com/watch?v=891jZr-7Mos&t=6s).

А теперь несколько слов об одной из последних работ Зюбина. В 2020 г. под его руководством был разработан текстовый язык для спецификации управляющего программного обеспечения poST (процесс-ориентированное расширение языка IEC 61131-3 Structured Text). Язык сочетает преимущества программирования на основе конечных автоматов с синтаксисом языка структурированный текст для программируемых логических контроллеров.

Вот публикации по этому вопросу:

1.Bashev V., Anureev I., Zyubin V. The Post Language: Process-Oriented Extension for IEC 61131-3 Structured Text / 2020 International Russian Automation Conference (RusAutoCon). Sochi. Russia. 2020, pp. 994-999, https://ieeexplore.ieee.org/document/9208049. Вот аннотация этой статьи: «This paper introduces a new programming language for control software specification. The language called poST is a process-oriented extension of the IEC 61131-3 Structured Text language widely used in the PLC domain. The poST language enables control software specification as a set of interacting FSM-based processes that have event-driven behaviour and operate with time intervals. The language is intended to provide a possibility to use the process-oriented approach for IEC 61131-3 users and comparing to the other process-oriented languages poST is easy to learn for the IEC 61131-3 community. An IDE for poST was developed with Eclipse (Xtext) toolset. Paper illustrates the poST language using for a hand dryer control software: we provide the source poST code and the generated C code for Arduino (ATmega 168) platform».

2. Zyubin V., Rozov A, Anureev I., Garanina N., Vyatkin V. poST: A Process-Oriented Extension of the IEC 61131-3 Structured Text Language // IEEE Access. 2022. https://ieeexplore.ieee.org/stamp/stamp.jsp?arnumber=9729833. Здесь есть две ссылки на наши работы.

Подходы, изложенные выше, развивает автоматное программирование и, возможно, кто-то из читателей настоящего текста захочет их опробовать и начать взаимодействовать с их авторами.

Кратко напомню о моем подходе к автоматному программированию. О нем можно прочитать в работах: «Автоматное программирование» (//vk.com/@1077823-vtomatnoe-programmirovanie">https://vk.com/@1077823-vtomatnoe-programmirovanie) и «Еще об автоматном программировании» (//vk.com/@1077823-esche-ob-avtomatnom-programmirovanii" title="https://vk.com/@1077823-esche-ob-avtomatnom-programmirovanii">https://vk.com/@1077823-esche-ob-avtomatnom-programmirovanii).

В заключение расскажу о наиболее широко внедренном направлении «моей» технологии автоматного программирования.

Еще в 2009 г. «с моей подачи» в ОАО «НПО «Аврора» Юрий Янкин начал использовать автоматное программирование для написания программ, реализуемых программируемыми логическими интегральными схемами (ПЛИС) (http://is.ifmo.ru/works/_jankin.pdf).

Янкиным и мною на основе автоматного программирования была разработана технология создания программного обеспечения модулей, выполненных на основе ПЛИС (http://is.ifmo.ru/present/2012/Yankin-Shalyto-PLIS.exe). При этом отмечу, что перед запуском эта презентация должна быть скачана. А вот то же «кино», представленное иначе: https://www.youtube.com/watch?v=YNWdmnwHZi8&t=29s.

Предложенная технология описана в следующих статьях: 1. Янкин Ю.Ю., Шалыто А.А. Автоматное программирование ПЛИС в задачах управления электроприводом // Информационно-управляющие системы. 2011. № 1, с. 50-56. http://www.i-us.ru/index.php/ius/article/view/13825. 2. Янкин Ю.Ю., Шалыто А.А. Применение автоматного подхода при программировании модулей управления шаговыми двигателями, выполненными на основе ПЛИС // Системы управления и обработки информации. 2011. Вып. 22, с. 92-103. https://elibrary.ru/item.asp?id=29426972. 3. Янкин Ю.Ю., Шалыто А.А. Метод создания программного обеспечения модулей, выполненных на основе программируемых логических интегральных схем // Системы управления и обработки информации. 2013. Вып. 26, с. 128-135. http://is.ifmo.ru/works/2013/yankin-ntkms.pdf. 4. Янкин Ю.Ю., Шалыто А.А. Разработка резервированного блока управления электроприводом на основе автоматного подхода // Научно-технический вестник информационных технологий, механики и оптики. 2014. № 6 (94), с. 146-152. http://is.ifmo.ru/works/2014/yankin-control-block.pdf.

С момента начала разработки технологии прошло двенадцать лет, и 28.10.2021 г. в диссертационном совете при ОАО «Концерн «НПО «Аврора» мой аспирант Ю.Ю. Янкин защитил кандидатскую диссертацию на тему «Технология разработки программного обеспечения автоматизированных систем управления электроприводом регулирующих органов судовых установок».

Несмотря на то, что эта технология базируется на покупном программном средстве Stateflow, технологии создания ПО для рассматриваемого класса систем, реализуемых на ПЛИС, не было, а теперь она есть. Под моим руководством в Университете ИТМО уже защищена не одна диссертация про автоматное программирование (http://is.ifmo.ru/disser/), но, чтобы внедрить этот подход в огромное число систем, такого даже близко не было. Трудно себе представить то число комиссий, которому Юрию пришлось сдавать эти системы на различных заказах. Когда на защите ему задали вопрос о научности работы, то мне показалось, что спрашивающий забыл утверждение Маркса: «Практика – критерий истины», о чем я в своем выступлении сказать не забыл :-). Кроме того, отвечая на вопросы, Юрий пообещал в ближайшие годы продолжить внедрять автоматный подход в судовые системы этого класса с той же интенсивностью. В заключительном слове Юра благодарил судьбу за встречу со мной.

В своем выступлении член Совета Б.В. Грек сказал, что ему однажды два часа сотрудник НПО «Аврора» Сергей Ванюшкин восторженно рассказывал об опыте применении автоматного программирования при создании ПО для судовых дизель-генераторов на программируемых логических контроллерах разных фирм при условии, что он не до не после программировать в классическом смысле этого слова не умел. Другой член совета – В.И. Поленин – вспомнил, что автоматный подход уже много лет применяет еще один наш сотрудник – Владимир Волобуев при создании ПО для информационно-управляющих систем, реализуемых на управляющих вычислителях (http://is.ifmo.ru/works/_volobuev.pdf). Член совета И.Р. Францев сказал, что у него в отделе под руководством еще одного моего аспиранта Антона Калачинского разработано инструментальное средство для поддержки автоматного программирования, которое широко используется для систем управления газотурбинными установками (https://www.avrorasystems.com/upload/iblock/cf3/cf3801161b1ca1a2fa7ba969079c45ec.pdf).

«Автоматный подход применительно к разработке ПО для судовых систем управления был предложен мною еще в 1991 г. В том же году произошло его первое внедрение – при создании системы управления дизель-генератора ДГР 500*500 судна проекта 15760 на базе аппаратуры Selma-2 фирмы ABB Stromberg. Программирование выполнялось на языке функциональных блоков, адаптированном под автоматное программирование» (http://is.ifmo.ru/books/switch/1). Несмотря на это, первая диссертация по автоматной тематике в НПО «Аврора» – диссертация Янкина – была защищена только через 30 (!) лет после этого события. Не зря говорят, что в России надо жить долго!

Перечень работ, посвященных формальной верификации «моих» автоматных программ, приведен в разделе 20 статьи «Автоматное программирование» (https://vk.com/@1077823-vtomatnoe-programmirovanie). При этом отмечу, что динамическую верификацию в форме тестирования для автоматных программ никто не отменял. При сдаче систем с автоматными программами они многократно верифицируются таким образом.

12.05.2022

 

Источники:

О развитии автоматного программирования – Анатолий Шалыто (Вконтакте, vk.com), 12 мая 2022.