Регистрация / Вход
Прислать материал

14.587.21.0032

Аннотация скачать
Постер скачать
Общие сведения
Номер
14.587.21.0032
Тематическое направление
Информационно-телекоммуникационные системы
Исполнитель проекта
федеральное государственное автономное образовательное учреждение высшего образования "Санкт-Петербургский национальный исследовательский университет информационных технологий, механики и оптики"
Название доклада
Разработка методов, средств и технологий проектирования, верификации и тестирования ответственных кибер-физических систем
Докладчик
Шалыто Анатолий Абрамович
Тезисы доклада
Цели и задачи исследования
Целью проекта является развитие научно-технической базы страны в области проектирования, верификации и тестирования ответственных кибер-физических систем посредством проведения исследований по приоритетным направлениям развития науки, технологии и техники в Российской Федерации с участием университетов Финляндии. Применение таких методов и средств повысит надежность, сократит сроки и стоимость построения и реконфигурации промышленных кибер-физических систем.

В рамках проекта поставлены следующие научно-технические задачи:
- Разработка архитектуры ответственных кибер-физических систем, сочетающей модели физических, вычислительных и коммуникационных процессов и феноменов. В рамках этой архитектуры будет раскрыта возможность таких систем менять конфигурацию в процессе работы.
- Генерация формальной модели объекта управления на основе его симуляционной модели. Процесс ручного построения формальной модели объекта управления сложен, поэтому планируется его автоматизировать.
- Обеспечение полноты представленности поведений объекта управления в примерах поведения, записанных на основе симуляционной модели. Чем больше различных поведений объекта управления записано на основе симуляций, тем более полную модель можно построить на их основе.
- Верификация систем в замкнутом цикле с использованием сгенерированных моделей объекта управления и интерпретация результатов верификации. Целесообразность использования и качество сгенерированных формальных моделей должны быть оценены.
- Тестирование систем в замкнутом цикле с использованием моделей объекта управления. Для учета модели объекта управления в процессе тестирования сам процесс тестирования будет рассмотрен на формальном уровне.
Актуальность и новизна исследования
Одним из наиболее трудозатратных процессов в промышленной автоматике является разработка, проверка корректности и поддержка программного обеспечения, использующегося в системах управления программируемых логических контроллеров и других вычислительных устройств. Известно много случаев, когда ошибки в программном и аппаратном обеспечении ответственных систем или в их архитектуре приводили к дорогостоящим и фатальным последствиям. Среди наиболее масштабных примеров - невыведение на орбиту исследовательского модуля “Полюс” ракетой-носителем “Энергия” (1987), а также авария ракеты-носителя Ариан 5 (1996) и катастрофа на АЭС Фукусима-1 (2011). Именно поэтому задача обеспечения корректности и безопасности контроллеров так важна.

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

В 2016 году в рамках проекта был разработан метод автоматической генерации формальных моделей объекта управления на основе примеров поведения замкнутой системы, полученных на основе осуществленных симуляций. Данный метод является эвристическим способом преобразования симуляционной модели системы (которая в рамках исследования предполагается доступной) в дискретную конечно-автоматную формальную модель. Метод включает в себя следующие этапы:

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

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

3. Сбор примеров поведения с запущенной симуляционной модели замкнутой системы. Симуляционная модель запускается заданное число раз со случайными значениями параметров из пункта 2.

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

5. Синтез модели объекта управления на основе дискретизированных примеров поведения. Рассмотрен синтез модели объекта управления в виде явного конечного автомата, а также в символьнов виде (то есть в виде набора ограничений).

6. Композиция синтезированной модели объекта управления с моделью контроллера. Сгенерированная модель объекта управления соединяется с моделью контроллера, которая предполагается доступной.

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

Описанный метод реализован на языке программирования Java. В качестве симуляционных сред поддерживаются среда NxtStudio для разработки приложений согласно промышленному стандарту IEC 61499, а также симулятор процессов Apros. В качестве верификатора, на языке которого в том числе генерируется модель объекта управления, используется символьный верификатор NuSMV.

Результаты исследования

Описанный метод был опробован в применении к двум моделям: к симуляционной модели лифта и к более сложной модели атомной электростанции. Для простоты рассмотрим применение метода к модели лифта. Эта модель реализована в среде NxtStudio, предназначенной для разработки приложений согласно промышленному стандарту IEC 61499. Модель состоит из модели самого объекта управления (лифта) и модели контроллера для него, при этом обе модели реализованы на основе функциональных блоков. Снимок экрана, показывающий часть реализации модели объекта управления и визуализацию его поведения, приведен на рис. 1.

Рис. 1. Симуляционная модель лифта в NxtStudio (снимок экрана).

В качестве входных параметров модель лифта принимает сигналы от контроллера, управляющего направлением движения лифта и открытием и закрытием дверей. Выходными параметрами являются состояния кнопок вызова, положение лифта, являющееся единственным целочисленным параметром (все остальные — булевы), и, для удобства программирования контроллера, параметры, обозначающие нахождение лифта на определенном этаже. Дискретизация положения происходила естественным образом — выделялись промежутки в случае нахождения на каждом этаже и между ними. Для сбора примеров поведения используется случайное изменение состояний кнопок лифта, что позволяет получать их полностью автоматически. Далее по результирующему сценарию строится модель, представляющая собой конечный автомат, в котором состояния соответствуют всем возможным значениям выходных параметров, а переходы — значениям входных параметров, то есть командам контроллера. На полученной модели были автоматически проверены некоторые LTL-свойства и были выявлены их нарушения: например, лифт не обязательно доезжает до этажа, на который был вызван.

Результаты применения метода к модели лифта хоть и являются предварительными, но демонстрируют возможность его использования в рамках задачи формальной верификации ответственных систем промышленной автоматики. Предложенный метод был сопоставлен с известными методами построения формальных моделей объекта управления или систем управления. В отличие от работы [Preuße, S. (2013). Technologies for Engineering Manufacturing Systems Control in Closed Loop (Vol. 10). Logos Verlag Berlin GmbH], где модель объекта управления предлагается строить в модульном виде, используя формализм сетей NCES (net-condition event systems), предлагаемый подход позволяет строить эту модель автоматизированно и избавляет пользователя метода от самостоятельного принятия решений по упрощению и дискретизации модели. Далее, в отличие от работы [Roth, M., Litz, L., & Lesage, J. J. (2010, June). Identification of Discrete Event Systems: Implementation Issues and Model Completeness. In 7th International Conference on Informatics in Control, Automation and Robotics (ICINCO) (Vol. 3, pp. 73-80)], где на основе методов теории формальных языков строятся модели всей замкнутой системы, рассматриваемый подход предназначен для генерации только модели объекта управления, что далее позволяет проверифицировать имеющийся контроллер. Кроме того, подход, предложенный в упомянутой работе, не рассматривается в контексте формальной верификации и обеспечения надежности ответственных систем.

 

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

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

Poster_template_IT.ppt