Международная конференция по промышленной автоматике INDIN включает сразу несколько тематических треков, среди которых киберфизические системы (CPS), интернет вещей (IoT) и промышленные агенты; облачные и беспроводные системы для промышленного применения; когнитивный и вычислительный интеллект; промышленная цифровизация, большие данные и планирование и другие. Одним из направлений конференции стали сессии, в рамках которых представители индустрии (Volkswagen, Phoenix Contact, TTTech и другие) презентовали свою работу в области автоматизации производства. На конференции обсуждались тенденции использования на производстве мультиагентных систем, цифровых двойников и технологий дополненной реальности, применяемых в обучении использованию систем, их ремонте и поддержке.
Выпускница кафедры компьютерных технологий Университета ИТМО и сотрудница международной научной лаборатории «Компьютерные технологии» Полина Овсянникова выступила с докладом в секции «Интеллектуальные технологии в системах промышленной автоматики» и рассказала о новом методе автоматической генерации формальных моделей объектов управления киберфизических систем при помощи активного обучения.
Киберфизической системой можно назвать систему, в которой физический компонент управляется программным. Примеры киберфизических систем — известные всем двигатель самолета, фрезерный станок или кофемашина. Киберфизические системы могут быть ответственными и требовать особенно тщательной проверки разработанной функциональности перед изготовлением финальной версии, так как ошибки в таких системах могут стоить не только денег, но и человеческих жизней. Другими словами, перед построением системы нужно проверить корректность работы спроектированной системы.
В большинстве случаев изначально разрабатывается симуляционная модель системы. Симуляционная модель повторяет функционал прототипа и является результатом моделирования процессов, протекающих в системе. Для проверки корректности ее поведения существуют два основных пути. Первый — запуск тестовых сценариев на симуляционной модели с целью проверки определенных свойств, которыми должна обладать система. Однако в данном случае нельзя гарантировать, что все сценарии были выполнены. Кроме того, запуск всех возможных сценариев займет очень много времени. Более надежный способ — формальная верификация.
«Наиболее действенный способ проверить правильность поведения системы — верификация. В этом случае мы строим формальную модель системы, которая должна быть по функциональности эквивалентна симуляционной. В моей работе в качестве формального представления был выбран конечный автомат. Зная, что у системы есть входные и выходные переменные, предположим, что каждая комбинация значений выходных переменных будет являться состоянием системы. Переходы из одного состояния в другое совершаются под действием комбинации значений входных сигналов. Таким образом, для совершения формальной верификации, мы создаем модель в виде конечного автомата, формулируем спецификации, загружаем все это в верификатор, который, например, строит автоматы по свойствам, которые мы задали, пересекает их с автоматом, представляющим систему и находит пути, которые противоречат указанным свойствам (контрпримеры). Преимущество такого способа заключается в том, что не нужно запускать сценарии вручную — мы должны лишь задать свойства, выполнение которых хотим проверить, а верификатор сам выявит контрпримеры при их наличии», — прокомментировала Полина.
Несмотря на все свои достоинства, у формальной верификации (особенно в замкнутом цикле, когда проверяется не только контроллер, но и объект управления) есть один главный недостаток — необходимость наличия формальной модели. Сегодня при проектировании киберфизических систем практически никто не занимается их созданием. Причина — формальные модели сложно сделать эквивалентными симуляционными и поддерживать в актуальном состоянии, их производство требует много времени, средств и высококлассных компетенций. Решить сложности можно с помощью построения формальной модели автоматическим способом. Помимо того, что такой подход сделает процесс создания формальной модели более быстрым и дешевым, существующие методы дают высокую гарантию того, что формальная модель эквивалентна симуляционной — при ручном создании вероятность несовпадения моделей гораздо выше.
«Киберфизическая система состоит из управляемого устройства — объекта управления и контроллера. Как правило, строится формальная модель контроллера, так как он является программным компонентом и может быть представлен в виде автомата. Конечно, бывают и исключения. Существуют также методы автоматической генерации модели контроллера. Труднее дело обстоит с объектом управления. Построить формальную модель объекта управления гораздо сложнее, так как, будучи физическим компонентом, он содержит непрерывные переменные, к примеру, уровень воды в баке, точная позиция какой-либо детали, температура и т.д. Кроме того, часто доступна только симуляционная модель объекта управления, которая, по сути, является “черным ящиком”. То есть мы можем только подать какие-то сигналы на вход и посмотреть, что будет на выходе. Вручную формальную модель объекта управления создавать еще тяжелее, чем модель контроллера, поэтому я занимаюсь разработкой метода ее автоматической генерации», — объяснила Полина.
Метод, предложенный Полиной Овсянниковой, отличается от существующих методов автоматического создания формальной модели объекта управления и основан на принципе активного обучения. Сегодня для построения формальных моделей объекта управления используются методы пассивного и активного обучения. В случае использования пассивного обучения перед запуском метода генерации необходимо собрать примеры поведения системы. Для этого симуляционная модель запускается, и ведется запись подаваемых ей на вход различных комбинаций входных сигналов и генерируемых в ответ выходных сигналов. Процесс записи примеров поведения может продлиться очень долго, а момент завершения не всегда очевиден. Затем записанные данные загружаются в программу, которая генерирует формальную модель на основе полученных данных.
Существенный недостаток пассивного обучения — возможные неточности в построении формальной модели, которая напрямую зависит от собранных данных. Так как момент завершения сбора данных, как правило, четко не обозначен, до некоторых состояний система может не дойти. Однако этот же метод имеет достоинства: если соединение с симуляционной моделью недоступно, то единственным возможным вариантом становится запись работы системы.
Методу активного обучения в качестве входных данных не требуются примеры поведения, нужны только информация о входных и выходных переменных системы и интерфейс взаимодействия с симуляционной моделью. При использовании такого подхода создание модели происходит в процессе взаимодействия с исходной системой, информация о том, какие сценарии нужно проверить и когда завершать построение, содержится в самом алгоритме. Сложность заключается в том, что объект управления может иметь непрерывные переменные.
Предложенный Полиной Овсянниковой метод реализует концепции активного обучения. Формальная модель строится в виде конечного автомата. Обнаружение новых состояний происходит при помощи алгоритма обхода графа в ширину. Для того, чтобы не допустить взрыва числа состояний из-за непрерывных переменных, их области значений подвергаются дискретизации. Как пример, если переменная принимает любые значения в области от 0 до 100, она может быть дискретизирована, то есть ее область значений может быть разбита на интервалы от 0 до 20, от 20 до 25 и от 25 до 100. Для того, чтобы учитывать при построении не непрерывные, а дискретизированные значения были разработаны два метода работы с такими переменными, которые доказали свою работоспособность и высокую эффективность при применении на практике.
Однако у разработки на сегодняшний день есть недостаток — конечный автомат получается большим, так как содержит много состояний и переходов, поэтому в формальном верификаторе на больших системах процесс верификации может занимать много времени. Сейчас ведется работа над получением модели с меньшим количеством переходов без потери точности.
