КАРТОЧКА ПРОЕКТА ФУНДАМЕНТАЛЬНЫХ И ПОИСКОВЫХ НАУЧНЫХ ИССЛЕДОВАНИЙ,
ПОДДЕРЖАННОГО РОССИЙСКИМ НАУЧНЫМ ФОНДОМ

Информация подготовлена на основании данных из Информационно-аналитической системы РНФ, содержательная часть представлена в авторской редакции. Все права принадлежат авторам, использование или перепечатка материалов допустима только с предварительного согласия авторов.

 

ОБЩИЕ СВЕДЕНИЯ

---

Номер проекта 22-29-01189

НазваниеВыделение классов спецификаций компонентов телекоммуникационных систем с пониженной сложностью решения задач идентификации состояний

Руководитель Евтушенко Нина Владимировна, Доктор технических наук

Организация финансирования, регион Федеральное государственное бюджетное учреждение науки Институт системного программирования им. В.П. Иванникова Российской академии наук , г Москва

Конкурс №64 - Конкурс 2021 года «Проведение фундаментальных научных исследований и поисковых научных исследований малыми отдельными научными группами»

Область знания, основной код классификатора 09 - Инженерные науки; 09-601 - Теория, методы проектирования и эффективность функционирования технических систем

Ключевые слова Формальные спецификации, неклассические трассовые модели, идентификация начального / текущего состояния, различающие, установочные и синхронизирующие последовательности, оценки сложности

Код ГРНТИ50.43.19

---

 

ИНФОРМАЦИЯ ИЗ ЗАЯВКИ

---

Аннотация
Развитие цифровых технологий привело к появлению большого количества электронных систем в различных областях нашей жизни; к таким системам можно отнести интерактивные сервисы, клиент-серверные приложения, различные микроконтроллерные системы и др., которые достаточно часто объединяют подсистемы от различных производителей, и, как правило, «не несут ответственности» за надежность передачи данных, полагаясь на сетевые возможности и «архитектурные» решения, предоставляемые пользователям. Поэтому практически для всех таких систем, в особенности использующих «чужие» разработки, необходимо обеспечить качественную проверку как функциональных, так и нефункциональных требований. Нарушение требований приводит к необходимости перепроектирования (частей) системы, что, так же как и проверка требований, невозможно без использования формальных методов. В этом смысле настоящий проект является продолжением проекта РНФ 16-49-03012, который выполнялся совместно с научной группой проф. Р. Джианга (Национальный университет Тайваня). В результате выполнения проекта, в том числе, с использованием алгоритмов решения задач идентификации состояний, были созданы сервисы по проверке функциональных требований к компонентам управляющих систем, поведение которых описано моделью классического конечного автомата [http://FSMTestOnline.ru, http://lctester.online]. Разработанными сервисами пользуются исследователи и преподаватели из восьми стран, как при проведении исследований, так и при проведении занятия по соответствующим предметам [http://www.tsu.ru/news/online-servisom-rff-uspeshno-polzuyutsya-uchenye-i/]. Однако для описания поведение (компонентов) реактивных управляющих систем часто используются и другие неклассические трассовые модели, такие как входо-выходные полуавтоматы, конечные автоматы, расширенные временными и другими аспектами, гибридные автоматы и др. Для таких моделей исследования по идентификации состояний и их использованию для проверки функциональных и нефункциональных требований для (компонентов) телекоммуникационных систем только начинаются. Идентификация состояний в трассовых моделях, называемых также автоматными моделями или моделями с конечным числом переходов, появившаяся как теоретическая область в классической теории автоматов, показала свою эффективность для проверки функциональных и нефункциональных требований для различных компонентов управляющих систем, таких как телекоммуникационные и киберфизические системы и др. Идентификация начального и /или текущего (достигнутого) состояния (моментального снимка / конфигурации) системы осуществляется на основе внешних наблюдений, т.е. без доступа к внутреннему состоянию системы. В режиме мониторинга даже частичное знание о текущем состоянии системы позволяет существенно упростить проверку функциональных и нефункциональных требований / свойств; в режиме верификации и тестирования знание текущего состояния позволяет проводить соответствующие проверки только в критических состояниях или состояниях, в которых затрачивается меньше тестовых усилий; в режиме логического синтеза предоставляется возможность использования «минимального» описания поведения системы, объединив неразличимые (при наблюдении за поведением системы извне) состояния в один блок. В настоящее время для описания и анализа больших трассовых систем разработаны эффективные компьютерные представления, такие как различные решатели, логические сети, древовидные представления, для эффективного использования которых накоплено большое количество программных средств, собранных в хорошо отлаженные библиотеки. Если поведение системы описано некоторой трассовой моделью, т.е. допустимыми последовательностями событий, то задача идентификации состояния системы ставится следующим образом. Необходимо синтезировать специальные входные / выходные последовательности (в ряде случаев называемые «умозрительными» экспериментами с системой), а именно, различающие, синхронизирующие и установочные идентификационные последовательности, что после подачи на систему входных последовательностей и наблюдении выходных реакций можно будет однозначно (или с некоторой допустимой точностью) определить начальное или текущее (достигнутое) состояние системы. Идентификация состояний достаточно хорошо изучена для классических конечных автоматов с детерминированным поведением. Известные точные (не эвристические) методы решения даже для классических конечных автоматов, как правило, доставляют идентификационные последовательности экспоненциальной длины относительно числа состояний/переходов автомата, а задачи проверки их существования и синтеза достаточно часто оказываются NP-трудными или даже PSPACE-полными. Однако поведение компонентов современных сложных систем, таких как протокольные реализации, сетевые сервисы и их композиции, компоненты киберфизических систем и программно-конфигурируемых сетей и др., могут быть описаны с требуемой точностью только неклассическими трассовыми моделями, такими как входо-выходные (расширенные и временные) (полу)автоматы, символьные и гибридные (полу)автоматы и др., для которых решение задачи идентификации состояний (если существует) является более сложным, чем для классических конечных автоматов. Несмотря на то, что в последнее десятилетие был получен ряд интересных результатов по анализу и синтезу идентификационных последовательностей для различных классов трассовых моделей, в получении которых авторы проекта приняли активное участие, для таких неклассических автоматных моделей практически все классы идентификации состояний исследованы достаточно слабо; более того, построенные идентификационные последовательности в общем случае имеют экспоненциальную длину относительно размеров системы. Последнее затрудняет практическое использование известных методов идентификации состояний для проверки функциональных и нефункциональных требований и оптимизации, и поэтому необходимо искать новые нетривиальные способы понижения длины идентификационных последовательностей для неклассических трассовых моделей. Одна из таких возможностей состоит в выделении классов трассовых моделей, таких, что, с одной стороны, худшие оценки длины идентификационных последовательностей для элементов этого класса гарантированно не достижимы, а с другой стороны, элементы таких классов соответствуют спецификациям (компонентов) телекоммуникационных систем. Данный проект призван выделить классы трассовых моделей, которые, с одной стороны, соответствуют спецификациям компонентов телекоммуникационных систем, а с другой стороны, допускают построение идентификационных последовательностей полиномиальной длины. Целью данной работы является исследование классов неклассических трассовых моделей, для которых можно понизить сложность построения и длину идентификационных последовательностей. Соответственно, можно сформулировать следующие основные задачи выполнения проекта. - 1: Исследование классов неклассических трассовых моделей, используемых в качестве спецификаций компонентов телекоммуникационных систем, для которых необходимо строить идентификационные последовательности; выделение классов неклассических трассовых моделей (временных, расширенных, автоматов, входо-выходных полуавтоматов), для которых существуют идентификационные последовательности полиномиальной длины. - 2. Исследование условий существования и построения идентификационных последовательностей для выделенных классов неклассических трассовых моделей. - 3: Экспериментальные исследования, иллюстрирующие возможность понижения сложности при решении проблем идентификации состояний для выделенных классов неклассических трассовых моделей. Проект разделен на два рабочих пакета (WPs). Рабочий проект WP 1 посвящен исследованию свойств спецификаций компонентов управляющих систем, для которых необходимо строить идентификационные последовательности, и выделению классов для неклассических автоматных моделей, для которых возможно понизить сложность процесса идентификации. Предполагается проведение экспериментальных исследований, иллюстрирующих возможность понижения длины идентификационных последовательностей для выделенных классов неклассических трассовых моделей. Основной целью рабочего проекта WP 2 является исследование условий существования и разработка методов синтеза различающих, установочных и синхронизирующих последовательностей для идентификации текущего / начального состояния системы для выделенных классов неклассических трассовых моделей; оценки длины идентификационных последовательностей для выделенных классов. С этой целью предполагается расширить теорию идентификации состояний для моделей с конечным числом переходов исследованиями, посвященными методам и оценкам сложности построения различающих, установочных и синхронизирующих последовательностей для идентификации начального и / или текущего состояния неклассических автоматных моделей, в том числе моделей с недетерминированным поведением, а также моделей, расширенных временными аспектами и другими специальными свойствами. Таким образом, в результате выполнения проекта будет проведен всесторонний анализ подходов к идентификации состояний для спецификаций компонентов управляющих систем, выделены классы неклассических автоматных моделей для построения идентификационных последовательностей, и разработаны новые подходы, основанные как на использовании классического дерева преемников и итерационном подходе, так и на использовании различных решателей (solvers) при решении задач идентификации состояний. Полученные в процессе выполнения проекта результаты будут опубликованы в рейтинговых журналах и представлены на международных конференциях. Совместная работа над проектом позволит молодым исследователям, участникам проекта, с одной стороны, получить полезный опыт от сотрудничества с всемирно известными экспертами в области анализа и синтеза трассовых моделей, а с другой, получить необходимую автономию при работе над целевыми задачами проекта.

---

 

ОТЧЁТНЫЕ МАТЕРИАЛЫ

---