Аннотация результатов, полученных в 2016 году
Согласно плану, в 2016 г. научная группа ТГУ исследовала параметры надежности, безопасности и доверия в сервисных системах или системах SaS, которые можно эффективно синтезировать и анализировать на основе классических и неклассических (полу)автоматных моделей. Основные результаты 2016 года сгруппированы по рабочим пакетам WP1-WP5. WP1: исследованы отношения между «классическими» проблемами логического синтеза и верификации и существованием синхронизирующих, установочных и различающих последовательностей для классических и неклассических конечных (полу)автоматов. В рамках рабочего пакета WP1, посвященного эффективным манипуляциям с конечно автоматными моделями с целью синтеза умозрительных экспериментов с классическими и неклассическими (полу)автоматами, в 2016 году были получены следующие основные результаты. 1) Метод проверки существования и синтеза для детерминированных полностью определенных автоматов различающих, синхронизирующих и установочных последовательностей (если таковые существуют) с использованием масштабируемых представлений в виде логических схем. 2) Программная реализация части предложенных методов проверки существования и синтеза умозрительных экспериментов на основе логических схем и результаты компьютерных экспериментов с использованием разработанного программного обеспечения с серией контрольных примеров (бенчмарок) из пакета ITC'99. При синтезе различающих последовательностей рассматривались схемы-мутанты, построенные внесением неисправностей трех типов: одиночные константные неисправности, неисправности «перемычек» и трудно обнаружимые неисправности при замене единичного набора вентиля схемы. В результате экспериментов строились различающие последовательности для каждого класса неисправностей, и оценивалась их длина. Различающие последовательности для пары начальных состояний автоматов, реализуемых схемами из пакета ITC’99, оказались достаточно короткими. Коллеги из ИСП РАН провели эксперименты по качеству построенных различающих последовательностей для покрытия переходов исходного расширенного автомата. Эксперименты показали, что для исходного расширенного автомата построенные различающие последовательности «покрывают» почти все простые пути, т.е. множество различающих последовательностей, построенное на «уровне» логических схем, может быть применимо на более высоком уровне абстракции. WP2: пакет посвящен исследованию параметров надежности для неклассических конечных (полу)автоматов и алгоритмам синтеза проверяющих тестов с гарантированной полнотой для недетерминированных, расширенных и временных автоматов. В рамках пакета WP 2 были получены следующие результаты. 1) Определен список основных параметров надежности систем SaS, которые могут быть проверены с использованием моделей с конечным числом переходов. К этим параметрам относятся: корректность функционирования, робастность системы, возможность восстановления системы после сбоя работы, чрезмерное потребление ресурсов реализацией сервисной системы. 2) Метод повышения полноты тестов, построенных по расширенному автомату. Полнота теста повышается за счет использования мутационного тестирования на основе инструмента mjava для программной реализации, выполненной по специальному шаблону. Предварительные эксперименты с рядом технических систем подтверждают, что такие тесты находят значительно больше функциональных ошибок в программных реализациях. 3) Метод построения адаптивной проверяющей последовательности для недетерминированных автоматов относительно редукции при условии, что автомат-реализация является детерминированным. Установлены достаточные условия, при которых предложенная адаптивная стратегия является исчерпывающей относительно всех возможных автоматов-реализаций. 4) Метод синтеза (адаптивных) проверяющих тестов с гарантированной полнотой для временных недетерминированных автоматов относительно редукции (для детерминированных автоматов относительно эквивалентности) в предположении, что известны максимальное число состояний проверяемого автомата и максимальная конечная граница для входных временных интервалов. Метод основан на построении соответствующей конечно автоматной абстракции временного автомата и дальнейшем использовании автоматных методов синтеза тестов с гарантированной полнотой. Показано, каким образом построенный тест можно существенно сократить, если все входные временные интервалы автомата-спецификации и автомата-реализации закрыты слева (или все интервалы закрыты справа). Дальнейшее сокращение проверяющего теста возможно за счет сокращения переходов в спецификации, т.е. за счет уменьшения степени недетерминизма спецификации. Несмотря на то, что в последнем случае построенный тест «перестает» быть полным относительно рассматриваемой модели неисправности, предварительные эксперименты показывают, что его полнота остается достаточно высокой. WP3: исследованы параметры для масштабируемых представлений (неклассических) автоматов, влияющие на безопасность и робастность веб-приложений. В рамках пакета WP3 были получены следующие основные результаты. 1) Определен список параметров, влияющих на безопасность изолированного web-приложения, поведение которого может быть описано конечно автоматной моделью. К этим параметрам относятся: превышение максимально допустимого значения внутренней переменной; достижимость критических ситуаций, потеря запроса/ответа, робастность, устойчивость к угрозам (утечки памяти, SQL-инъекции и др.), состязания между пользователями. Сервисные системы могут быть адекватным образом промоделированы подходящими недетерминированными, возможно, ненаблюдаемыми автоматами; далее может быть синтезирован проверяющий тест для проверки корректной реализации критических (с точки зрения параметров безопасности) переходов. 2) Для совместной работы веб-приложений установлены достаточные условия для обнаружения тупиковых ситуаций и осцилляций в композиции конечных автоматов, если компоненты композиции являются детерминированными, возможно, частичными автоматами, и предложен двухэтапный алгоритм для определения тупиковых ситуаций. Предложен более простой подход, чем ранее известные, к построению композиций автоматов с таймаутами. После того как построена параллельная композиция подходящих автоматных моделей для SaS, композиция может эффективно анализироваться для проверки критических свойств безопасности. WP4: исследованы параметры сервисных систем, которые влияют на поведение компоненты и методы синтеза тестов для формирования данных при прогнозировании уровня доверия на основе проверки функционирования. В рамках WP4 получены следующие основные результаты. 1) Предложен подход упреждающей оценки доверия, который содержит два основных этапа. Первый этап заключается в определении параметров, которые могут повлиять на доверие к системе (потенциально «чувствительные» параметры доверия, которые могут быть получены от экспертов). Второй этап основан на «извлечении» значений чувствительных параметров доверия по анализу исходного кода исследуемой системы и при подаче построенных тестов. 2) Для оценки доверия предложен подход на основе методов и средств активного тестирования. Идея предлагаемого подхода заключается в том, чтобы влиять на поведение тестируемой реализации за счет подачи конкретных входных сигналов, которые могут «заставить» тестируемую систему показать себя как не заслуживающую доверия. Тестовые наборы, на которых проверяется поведение тестируемой системы, могут быть получены различными способами, начиная от случайного моделирования, методов и средств статического анализа и заканчивая типовыми методами генерации тестов на основе формальных моделей. WP5: исследованы параметры, необходимые для выполнения функциональных и нефункциональных требований и новые методы к доопределению систем частичных булевых функций для получения оптимальных (или близких к оптимальным) логических схем (относительно предсказания уровня удовлетворенности конечного пользователя). В рамкахWP5 получены следующие основные результаты. 1) Исследованы параметры различных электронных сервисов, имеющих наибольшее влияние на удовлетворенность конечного пользователя. Отмечено, что параметры, необходимые для выполнения функциональных и нефункциональных требований, определяются индивидуально для каждого сервиса (или групп сервисов). Оценка удовлетворенности конечного пользователя QoE в мультимедийных системах обычно производится на основе сетевых параметров; к таким параметрам относятся, например, число потерянных пакетов при передаче данных (packet loss), а так же «дрожание» транслируемого изображения (jitter). Для OTT (Over-the-Top) сервисов, передающих по телекоммуникационной сети некоторое видео по требованию пользователя и не отвечающих за качество связи и другие сетевые параметры, критическими можно считать количество данных, передаваемых в единицу времени, или битрейт, время буферизации видео, «замерзание» изображения (freezing events), т.е. количество «заморозок» и общее/максимальное время такой «заморозки»/буферизации. С ростом развития концепции «Интернет вещей» (Internet of Things или IoT) все большее внимание уделяется нефункциональным параметрам, в частности, бизнес-параметрам, а также параметрам, связанным с влиянием на окружающую среду, в частности, потреблением ресурсов, и т.п. 2) Предложен метод доопределения системы частичных булевых функций для получения оптимальных (или близких к оптимальным) логических схем (относительно предсказания уровня удовлетворенности пользователя). Метод опирается на использование самообучающихся систем для предсказания / оценивания QoE, основанных на дереве решений (Decision Tree), одним из масштабируемых представлений которого являются логические схемы. Оптимизация логической схемы осуществляется за счет «оптимального» или близкого к нему доопределения системы частичных булевых функций, соответственно, в рамках WP5 был предложен метод такого доопределения (с использованием системы проектирования и верификации логических схем ABC). На основе предлагаемого подхода с использованием логических схем были продолжены эксперименты для предсказания результативности обучения иностранному языку по выбранной методике. Предварительные эксперименты с обучающей и тестовой выборками показали, что в 88% оценочные значения определились корректно с допустимой погрешностью предсказания, что свидетельствует о достаточно хороших перспективах использования описанных выше критериях оптимизации логических схем. 3) Предложен подход к оптимизации потребления энергии, затрачиваемой при использовании встроенного программного обеспечения, основанный на манипуляциях с моделями с конечным числом состояний/переходов, которые могут быть получены по исходному программному коду. В качестве критерия оптимизации рассматривается сетевая нагрузка при использовании различных программных реализаций сетевых компонентов, в частности, при различной реализации сетевых протоколов. Соответственно, был предложен подход, основанный на оптимизации исходного кода с использованием модели взвешенного древовидного автомата (Weighted Tree Automata или WTA). Метод содержит правила выбора весов для переходов автомата с целью оптимизации сетевых обменов для снижения энергопотребления/нагрузки сети. После того, как все функции записи или чтения (на переходах WTA) сгруппированы, выбирается оптимальная последовательность доступных замен для регулярных цепочек. Предложенный подход может оказать существенное влияние на энергопотребление, например, при использовании аппаратных компонентов, реализующих алгоритмы шифрования. При выполнении работ по проекту в 2016 г. сделаны 6 докладов на международных конференциях с публикацией докладов в изданиях, входящих в Scopus и Web of Science, опубликованы 4 журнальные статьи. Для эффективного обмена результатами, полученными при выполнении проекта в 2016 г., для их анализа и обобщения проведен совместный семинар (Национальный университет Тайваня, Тайбэй, 2-9 декабря, 2016).

Аннотация результатов, полученных в 2017 году
Согласно плану, в 2017 г. научная группа ТГУ продолжала исследования по разработке масштабируемых методов для обеспечения критериев безопасности, надежности и доверия SaS, в соответствии с техническим заданием на проект (по рабочим пакетам WP 1-5). Кроме того, в отчетном периоде мы рассмотрели еще один тип сервисов, а именно, сервисы, направленные на эффективную обработку, передачу и хранение информации. В рамках рабочего пакета WP 1, посвященного эффективным манипуляциям с конечно автоматными моделями, в 2017 году научная группа ТГУ остановилась на масштабируемом синтезе последовательностей, идентифицирующих состояния автоматов, с использованием квантифицированных булевых формул (QBF), большинство решателей для которых основаны на логических схемах, а также на получении теоретических результатов по упрощению входо-выходных полуавтоматов и временных автоматов с целью дальнейшего синтеза экспериментов, решения задач тестирования и верификации и др. В 2017 г. были получены следующие основные результаты. 1) Теоретические и экспериментальные результаты по синтезу установочных последовательностей на основе квантифицированных булевых формул, для которых было проведено экспериментальное исследование четырех QBF решателей, а именно, DepQBF, RAReQS, QELL и 2QBF решателя, встроенного в систему АВС. Построение адаптивной установочной/синхронизирующей последовательности опирается на эффективный синтез установочных тестовых примеров для каждой пары состояний, и, принимая во внимание результаты экспериментов по синтезу установочных последовательностей на основе QBF решателей, мы предлагаем совместить два подхода. Мы предлагаем проверить на выполнимость соответствующую QBF формулу только для пар состояний, что должно быть значительно эффективнее, чем проверять такую формулу сразу для всех состояний. 2) Предложен метод синтеза адаптивных синхронизирующих последовательностей для детерминированных неприведенных автоматов. 3) Методы построения установочных и синхронизирующих последовательностей для автоматов адаптированы для построения установочных и синхронизирующих последовательностей для входо-выходных полуавтоматов. 4) С использованием конечно автоматной абстракции предложен метод минимизации детерминированного временного автомата, который является автоматом, приведенным по состояниям и времени. Показано, что минимальная форма детерминированного полностью определенного временного автомата единственна (с точностью до изоморфизма), т.е. может рассматриваться в качестве канонической формы такого автомата для временных автоматов. 5) В 2017 г. усовершенствованы программные пакеты BALM-II и FSMTest, которые используются при организации работ по пакетам WP 1–5; в пакеты добавлены новые команды и новые программные реализации, осуществляющие манипуляции над автоматами. В отчетном году по рабочему пакету WP2 было продолжено исследование корреляции между тестами для логических схем, построенными на различных уровнях абстракции, а также проведено экспериментальное исследование качества тестов, построенных на основе расширенного и временного автоматов относительно проектно-ориентированных мутантов. В 2017 году мы также рассмотрели еще один тип сервисов, а именно, сервисы, направленные на эффективную обработку, передачу и хранение информации, и исследовали подходящие в данном случае модели неисправности. Эта часть исследований (начаты в 2017 г.) относится к тестированию и верификации программируемых сетей, которые формируют «сервис по требованию» (service-on-demand). Были получены следующие основные результаты. 1) В результате проведенных экспериментов для схем из пакета ITC’99 было показано, что для логических схем тесты, построенные конечно автоматными методами, являются достаточно качественными; более того, тест, основанный на поиске кратчайшей различающей последовательности для двух схем, спецификации и мутанта, после минимизации оказался даже длиннее, чем тест, основанный на выборе псевдослучайной (различающей) последовательности. Наиболее эффективным (в смысле длины построенного теста с гарантированной полнотой) является комбинированный подход, в котором на первом этапе запускается случайная генерация; далее тест «достраивается» различающими последовательностями для обнаружения не обнаруженных ранее неисправностей. 2) В отчетном году мы использовали расширенный автомат для тестирования бизнес-параметров сервиса, предоставленного компанией Loymax, которая занимается автоматизацией программ лояльности, направленных на реализацию комплекса маркетинговых мероприятий для привлечения новых клиентов и других видов потенциального прибыльного развития. Для протокола взаимодействия кассового ПО с системой Loymax был построен расширенный автомат, по конечно автоматному срезу которого обходом графа переходов был построен тест. Анализ результатов тестирования позволил обнаружить ряд ошибок и несоответствий тестируемой реализации спецификации протокола, некоторые из которых оказались критическими, в смысле возможных финансовых убытков компаний. Отметим, что тестируемая система на момент ее анализа лишь подготавливалась к релизу; соответственно, обнаруженные ошибки были устранены до ее реализации на реальных серверах. 2) На основе модели временного автомата были проведены эксперименты по качеству тестов, построенных конечно автоматными методами для проверки функциональных и нефункциональных требований к (встроенному) программному обеспечению (кибер) физических систем, используемых в лазерных сервисных системах, которые позволяют наблюдать за удаленными объектами и процессами, осуществлять мониторинг на линии с высокой скоростью и др. Как показали проведенные эксперименты (с использованием мутационного тестирования), для сервисных систем «генераторного» типа, тесты, построенные по таким моделям, оказываются достаточно качественными. 3) Мы также рассмотрели ошибки в реализациях телекоммуникационных протоколов, соответствующие ошибкам переходов / выходов недетерминированного автомата-спецификации. Экспериментально показано, что мутанты, соответствующие реальным ошибкам в программных реализациях протокола, достаточно часто можно обнаружить тестами полиномиальной длины с использованием новой модели неисправности, основанной на наблюдаемых проекциях. Еще одна новая модель неисправности для недетерминированных автоматов основана на сокращении автомата-спецификации таким образом, чтобы в сокращенном автомате существовала адаптивные различающая и передаточные последовательности. Предложен метод выделения из исходного автомата близкого к максимальному подавтомату с такими свойствами. 4) Исследование платформы для виртуализации сервисов и функций предполагает, что все компоненты должны быть тщательно протестированы, что, в свою очередь, требует использования не только привычных (классических) моделей неисправности, но и введения новых моделей неисправности. В этом году мы сконцентрировались на проверке цепочек сервисных функций (SFCs), которые запрашивает пользователь, сформулировали цели и задачи тестирования и предложили модель неисправности, основанную на перечислении графов. 5) На первом этапе тестирования композиция взаимодействующих систем проверяется на возможность совместного функционирования, т.е. на отсутствие осцилляций и тупиковых ситуаций. Для компактного задания множества «неисправных» композиций мы используем мутационные автоматы, полученные в результате всевозможных доопределений неопределенных переходов в каждой компоненте. Данная модель неисправности использована для композиции автоматов с таймаутами, для которой проверяющий тест строится с использованием усовершенствованного пакета BALM-II. 7) Проверка возможного достижения критических состояний и/или критических значений переменных в расширенном автомате хорошо осуществляется с использованием различных верификаторов, таких как, например, JavaPathFinder (JPF). Для реализации расширенного автомата мы используем шаблонный перенос инструкций в Java код, сохраняя все контекстные переменные, предикаты, описывающие условия переходов, и состояния расширенного автомата, соответствующие рабочему режиму. Соответственно, достижимость критических значений и/или состояний сохраняется и в шаблонной реализации. Затем, используя верификатор JPF, предназначенный для проверки многопоточных программ, мы можем автоматически проверить, могут ли произойти опасные ситуации в проверяемом веб-сервисе. Данный подход был предложен в рамках рабочих пакетов WP 2 и 3 и был опробован на специальной группе игровых сервисов. В рамках рабочего пакета WP3 мы продолжили разработку алгоритмов для проверки безопасности веб-приложений и мобильных сервисов, в том числе, для композиций автоматов с входными и выходными таймаутами. Кроме того, были исследованы методы построения композиций временных и расширенных автоматов, проблемы, возникающие при построении таких композиций, и предложены подходы к их решению. Были получены следующие основные результаты. 1) Полученные в 2016 г. условия для анализа возможности возникновения тупиков и осцилляций в бинарной параллельной композиции конечных автоматов переформулированы для автоматов с входными и выходными таймаутами. 2) С использованием верификатора javaPathFinder для мобильных приложений (JPF- mobile) были обнаружены уязвимости в мобильных приложениях. 3) Один из способов исследования уязвимостей в веб приложениях заключается в построении полуавтомата, представляющего «опасные» последовательности символов и соответствует решению полуавтоматного неравенства или уравнения относительно операции конкатенации. Решение неравенства может привести к ложным срабатываниям, что, вообще говоря, может привести к недовольству пользователей при дальнейшей санитизации, поскольку при санитизации будет удаляться то, что на самом деле вредоносным не является. При решении полуавтоматного уравнения возможны пропуски опасных пользовательских данных. Нами получены новые результаты по решению полуавтоматных уравнений / неравенств относительно конкатенации, сформулированы достаточные условия, при которых полуавтоматное уравнение / неравенство не имеет решений или имеет несколько попарно не эквивалентных решений. 4) Мы также отмечаем, что в результате выполнения работ по проекту в 2017 г. показано, что в ряде случаев для описания временным автоматом совместной работы временных автоматов недостаточно условий отсутствии осцилляций и наличия медленной внешней среды. Необходимы дополнительные условия, некоторые из которых уже исследованы, другие мы продолжаем исследовать. В рамках рабочего пакета WP 4 научная группа Томского государственного университета продолжает исследования в области оценивания и предсказания уровня доверия для сервисных систем. В 2017 году основной упор был сделан на так называемые устройства с ограниченными вычислительными возможностями, причем с развитием «Интернета вещей» (IoT) возрастает актуальность исследования таких устройств. В 2017 году получены следующие основные результаты. 1) Адаптация метода предсказания доверия на основе логических схем с использованием известных методов и средств машинного обучения. Предлагается при синтезе логической схемы, оценивающей уровень доверия и имеющей один выход, на котором появляются булевы константы 0 (не доверяю) и 1 (доверяю), «консультироваться» с некоторой «идеальной» или «золотой», но недостаточно масштабируемой самообучающейся моделью, что позволит существенно усовершенствовать процесс проектирования логической схемы. 2) Выявление критических параметров для мобильных приложений и устройств с целью проектирования логической схемы для оценки уровня доверия для мобильных приложений и смартфонов с ограниченными вычислительными возможностями. В отчетном году мы остановились на следующих динамических параметрах мобильных приложений: 1) размер «кучи» – размер занимаемой приложением памяти при ее динамическом распределении; 2) размер стека – размер памяти, занимаемой выделенным потоком приложения; 3) загрузка процессора – загрузка приложением ЦП, исчисляемая в процентах; 4) загрузка (использование) диска – пространство, занимаемое данными приложения; 5) потребление энергии – количество энергии, потребляемой приложением. Для моделирования различных комбинаций значений параметров при вычислении уровня доверия мобильному приложению мы предлагаем использовать самообучающиеся модели. Более того, поскольку мы рассматриваем смартфоны с ограниченными вычислительными возможностями, предлагается использовать масштабируемые представления таких моделей, а именно, логические схемы. Проведенные нами предварительные эксперименты свидетельствуют, что для определенных выше параметров и ограничений на их значения описанный выше подход представляет интерес. При оценке / прогнозировании QоЕ (рабочий пакет WP5) мы используем масштабируемые представления, такие как логические схемы, а также различные булевы выражения, которые описываются такими схемами. Исследованы свойства логических схем, которые можно использовать для повышения их способности к предсказанию уровня удовлетворенности пользователей композитных сервисов. Кроме того, в этом году мы рассмотрели новые типы сетевых сервисов, направленных на организацию хранения и передачи информации, и определили ряд параметров, которые влияют на качество обслуживания при использовании таких сервисов. Получены следующие основные результаты. 1) Часть недостатков интервального доопределения логической схемы при прогнозировании уровня QoE (результаты отчета 2016 г.), как и в случае прогнозирования уровня доверия, может быть устранена за счет «консультирования» при синтезе логической схемы с некоторой «идеальной» или «золотой» технологией обучения (или подходящей, но недостаточно масштабируемой самообучающейся моделью). Для двух выбранных «эталонных», но недостаточно масштабируемых самообучающихся моделей, используемых для предсказания значения QoE, мы предлагаем построить и совместить параллельно такие логические схемы. Выходные значения, снимаемые со схем-компонент, подаются на схему, вычисляющую минимальное (максимальное) значение двух целых чисел. Построенная таким образом схема гарантирует, что предсказываемое значение QoE будет не ниже (не выше), чем значение, возвращаемое каждым из «оракулов». 2) Были также исследованы и другие возможности совмещения двух логических схем, в зависимости от их «предсказательных» способностей, при условии, что каждая из этих схем детерминирована в сторону фиксированного ответа QoE. В этом случае значение QoE параллельно вычисляется на обеих логических схемах; на выходе схемы-композиции выдается значение лишь одной из них, и для этого можно воспользоваться подходящим мультиплексором для «снятия» значений с требуемых выходов, а также переключателем для указания ситуаций, при которых выходная реакция должна «сниматься» с той или иной схемы. 3) В отчетном году мы кратко рассмотрели параметры (запросов), влияющие на качество обслуживания и, как следствие, удовлетворенность пользователя / клиента сервисами специального типа, а именно, сервисами для эффективной обработки, передачи и хранения информации. Мы идентифицируем основные параметры запросов, которые влияют на качество обслуживания пользователя, и рассматриваем функциональные или логические параметры и параметры, относящиеся к распределению ресурсов. Значения параметров первой группы проверяются с использованием масштабируемых операций над булевыми матрицами; параметры второй группы можно проверить с помощью соответствующей системы логических выражений. Для проверки качества запросов, направляемых на одну из платформ по виртуализации, мы провели эксперименты с парсером, «разбирающим» запросы в языке TOSCA, чтобы убедиться, что в настоящий момент парсер «пропускает» запросы, для которых невозможно обеспечить требуемое качество обслуживания; более того, некоторые запросы угрожают безопасности системы. Выполнение работ по Российско-Тайваньскому проекту полностью соответствует заявленному плану исследований. Результаты, полученные в процессе выполнения работ по проекту, опубликованы в 15 работах (одна публикация совместно с научной группой Национального Университета Тайваня), в том числе, 8 – в журналах и периодических изданиях (5 входят в международные базы цитирования Scopus и Web of Science и 3 – в Перечень ВАК), 7 – в трудах международных конференций (все входят в международные базы цитирования Scopus или Web of Science); защищена 1 кандидатская диссертация (под руководством руководителя проекта РНФ).

Аннотация результатов, полученных в 2018 году
Как отмечалось в отчетах 2016, 2017 гг., понятие системы как сервиса (SaS) является, вообще говоря, новой концепцией, которая направлена на расширение существующих «облачных» технологий для любых типов систем с целью их использования в качестве (электронных) услуг. В 2018 г. мы продолжили исследования по разработке масштабируемых методов для обеспечения критериев безопасности, надежности и доверия SaS согласно техническому заданию по проекту; кроме того, в соответствии с планом исследований, мы посвятили данный этап разработке программных и/или аппаратных реализаций для предоставления сервисных систем по тестированию / оценке качества / доверия. Рабочий пакет WP1. В рамках рабочего пакета WP1, посвященного эффективным манипуляциям с конечно автоматными моделями с целью синтеза умозрительных экспериментов с классическими и неклассическими автоматами, в 2018 году научная группа ТГУ продолжила развитие масштабируемых методов идентификации состояний конечных автоматов на основе последовательностных схем с использованием различных формул с кванторами (совместно с Тайваньским партнером), развитие эффективных адаптивных стратегий для этой цели, а также проанализировала влияние частичности и адаптивности на сложность различающих, установочных и синхронизирующих экспериментов с классическими автоматами, поскольку описания большинства сервисных систем определены лишь частично, и частичность и адаптивность можно рассматривать как две силы, работающие в противоположных направлениях; в некоторых случаях адаптивность может упростить построение умозрительных экспериментов с классическими и неклассическими автоматами. Предложенные подходы к построению установочных и различающих (адаптивных) последовательностей были опробованы на элементах сервисных систем, в частности, на системе итальянской железнодорожной компании, позволяющей пассажирам получать компенсации в случае задержки поездов. Рабочий пакет WP2. В рамках развития концепта «все как сервис» (англ. – anything as a service) представляют интерес программные разработки, которые предоставляют пользователю возможность запрашивать услуги по синтезу тестов для различных типов спецификаций. Мы реализовали ряд сервисов по тестированию дискретных систем; были выбраны следующие спецификации для включения в сервисы по синтезу тестов: классические конечные автоматы, расширенные автоматы, последовательностные и комбинационные логические схемы. Сервисы предварительно опробованы как сотрудниками научной группы, так и студентами ТГУ. Сервис по построению тестов для конечных детерминированных автоматов FSMTestOnline.ru включает построение тестов с гарантированной полнотой на основе моделей «белого и черного ящиков». Для модели "белого ящика" генерируются все одиночные мутации функций переходов и выходов; построенные последовательности объединяются в единый тест. Для модели «черного ящика» предъявленный автомат-спецификация проверяется на наличие необходимых свойств, таких как детерминированность, связность, и др.; тесты строятся обходом графа переходов и HSI-методом. Сервис по синтезу тестов для расширенных автоматов также включает построение тестов с гарантированной полнотой на основе моделей «белого и черного ящиков». Кроме того, пакет по расширенным автоматам позволяет вывести диаграмму переходов расширенного автомата, заданного пользователем, если заданный автомат не слишком большой, и сохранить данный автомат для построения тестов. Сервис по синтезу тестов на основе логических схем lctester.online в некотором смысле дополняет предыдущий, расширяя возможности пользователя при задании формальных спецификаций, и основополагающей моделью в данном случае выступает комбинационная или логическая схема. Тесты строятся на основе модели «белого ящика», при этом рассматриваются три типа возможных ошибок: одиночные константные неисправности, неисправности перемычек и трудно обнаружимые неисправности, изменяющие значения одного бита на одном входном наборе функционального элемента. Различающая последовательность для каждого из мутантов синтезируется с использованием средств верификации системы ABC (интегрирована в сервис). Данный сервис по синтезу тестов на основе логических схем может быть очевидным образом использован для синтеза тестов относительно модели классического детерминированного автомата. В этом случае необходимо обратиться к подходящему логическому синтезу, в случае, когда задание на синтез предоставляется в виде конечного автомата. Такая опция также предусмотрена в данном сервисе. В рамках рабочего проекта WP 2 мы также рассмотрели новые модели неисправности и предложили методы синтеза тестов с гарантированной полнотой на их основе. В этом году мы предложили так называемый гибридный подход к построению проверяющего теста для цифровой схемы. На первом шаге по заданной логической схеме строится тест, обнаруживающий одиночные константные неисправности, неисправности «перемычек» и трудно обнаружимые неисправности, изменяющие выходное значение вентиля на одном входном наборе. На втором шаге, если по логической схеме можно построить автомат, то тест достраивается до обхода графа переходов построенного автомата или любого другого «автоматного» теста с гарантированной полнотой; как известно, такой тест обнаруживает большое количество функциональных ошибок в реализации системы. Если построить конечный автомат по логической схеме не представляется возможным, то устанавливается модель неисправности, относительно которой построенный тест является полным. Часть работ по пакету WP 2 была посвящена исследованию новых моделей неисправности для дискретных (сервисных) систем. Поскольку частичность является характерной особенностью спецификаций таковых, например, сетевых протоколов, при реализации системы неопределенные переходы доопределяются некоторым образом, и нужно проверить, что при таком доопределении не возникает осцилляция. Для описания возможных реализаций используются мутационные автоматы, содержащие на неопределенных переходах возможные реализации этих переходов. При композиции возникает переход в состояние ОСЦИЛЛЯЦИЯ, если осцилляция возможна для реализаций, переводящих композицию в данное состояние. Полный проверяющий тест должен содержать входные последовательности, которые «покрывают» каждый переход композиции в состояние ОСЦИЛЛЯЦИЯ, и построение такого теста не является тривиальной задачей для недетерминированного автомата, каковым является композиция мутационных автоматов. Мы уточнили понятие проверяющего теста на осцилляции, добавляя в тестовые последовательности, помимо входных воздействий, время ожидания выходных реакций, и, соответственно, уточнили понятие композиции для оценки таймаута при ожидании выходного символа. Мы также предложили новый метод построения тестов с гарантированной полнотой для инициальных автоматов с таймаутами. В отличие от классических автоматов, минимальная форма инициального автомата с таймаутами не является единственной (с точностью до изоморфизма), и, более того, минимальные формы одного автомата могут иметь различное число состояний. Соответственно, мы предложили метод синтеза проверяющего теста для автоматов с таймаутами относительно модели неисправности, где спецификацией является конечно автоматная абстракция, а область неисправности содержит каждый автомат с таймаутами, такой, что минимальная форма его конечно автоматной абстракции имеет не более m > 1 состояний. Продолжено исследование сервисов, направленных на эффективную обработку, передачу и хранение информации. Предложены модели неисправности для тестирования архитектуры SDN и методы синтеза тестов с гарантированной полнотой на их основе. Установлено следующее. а) Набор параметризованных путей, в котором для каждой упорядоченной пары (h1, h2) различных хостов h1 и h2 множество TS содержит параметризованный путь, который начинается в h1 и заканчивается в h2, является hc-полным тестом относительно <=, FD>, где = - отношение равенства, а область неисправности FD содержит возможные реализации виртуальных путей. б) Набор параметризованных путей, в котором для каждой пары двух соседних коммутаторов (s1, s2) множество TS содержит параметризованный путь, имеющий ребро (s1, s2), является sc-полным тестом относительно <=, FD>. в) Набор параметризованных путей, в котором для каждого коммутатора s_i каждая пара его соседних узлов n_j и n_k и каждого хоста d существует путь из класса (s_i, n_j, n_k, d)-эквивалентности, является sf-полным тестом относительно <=, FD>. Рабочий пакет WP3. В этом году мы рассматривали построение тестов относительно робастности и безопасности, которые во многих случаях строятся для композиций классических и неклассических автоматов. Были расширены возможности построения композиций расширенных автоматов без перехода к конечно автоматным абстракциям, исследованы проблемы, возникающие при построении параллельных композиций для временных автоматов, и предложены подходы к их решению. На основе автоматной модели предложен метод синтеза тестов относительно робастности; проведены исследования по анализу качества тестов, построенных по автоматным моделям, для обнаружения тупиков и осцилляций в композициях программных реализаций телекоммуникационных протоколов. Эксперименты проводились со студенческими реализациями различных протоколов: клиентское и серверное приложения протокола разрабатывались различными студентами, и их совместная работа проверялась на наличие осцилляций (рабочий пакет WP 2). Если осцилляции в композиции отсутствовали, то в одну из компонент вносились достаточно простые мутации, и получившаяся композиция снова проверялась на наличие осцилляций. Все осцилляции, возникающие при таких мутациях, были обнаружены подходящими тестами. Более того, тест на осцилляции обнаружил также некорректную работу с памятью, т.е. тесты, построенные для проверки взаимодействия, в данном случае позволили обнаружить проблемы безопасности/надежности реализации. Продолжены исследования в области поиска уязвимостей для веб сервисов на основе решения (полу-) автоматных неравенств и уравнений. Для определения множества входных последовательностей, которые могут привести к успешной атаке, Тайваньские коллеги используют функции PreConcatSuffix и PreConcatPrefix, аналогичные нахождению левого и правого частного и общего решения полуавтоматного неравенства относительно операции конкатенации. Установлено, что подход на основе правого/левого частного дает возможность выявить возможные уязвимости, однако может привести к ложным сигналам о наличии уязвимостей (ложные срабатывания). На основе полученных результатов предложены два подхода к поиску более точного (с точки зрения последующей санитизации) решения. Мы рассмотрели некоторые распространенные атаки на веб сервисы, а именно, SQL-инъекции и XSS-атаки, и проиллюстрировали, каким образом можно обнаружить уязвимости на основе нахождения правого/левого частного, т.е. на основе решения полуавтоматных неравенств. Удалось, в частности, обнаружить уязвимость на сервисе электронного расписания ТГУ. Получен ряд результатов в области санитизации пользовательских данных (работы неотъемлемо сопряжены с анализом уязвимостей веб сервисов). Для распознавания входных данных, представляющих различные атаки, мы попробовали использовать технологию машинного обучения, например, нейронную сеть, которая по введенным пользователем данным распознает, являются ли данные безопасными, и если нет, то при введении данных в какое поле заданная атака может быть реализована. Эксперименты по созданию и обучению подходящей нейронной сети проводились на основе SQL-инъекций и XSS-атаки; для создания нейронной сети использовался инструмент «Keras over TensorFlow». Для обучения нейронной сети была сгенерирована обучающая выборка: миллион различных строк с XSS-атаками, миллион различных строк с SQL-инъекцией вида «;‘OR 1= 1’», миллион различных строк с SQL-инъекцией общего вида. Каждая строка с атакой маскировалась случайными текстовыми данными. Были сгенерированы строки, которые «похожи» на атаки, но таковыми не являются (вместо тега <SCRIPT>, указывался несуществующий тег <ASCRIPT> и т.п.). Таких псевдо атак было сгенерировано три миллиона (по одному миллиону для каждого вида атаки). Были сгенерированы просто текстовые строки (вновь один миллион), длина строк в каждом случае была 100 символов. После обучения сети на 10% такой искусственно сгенерированной выборки нейронная сеть классифицировала угрозы с точностью 99,97%. Рабочие пакеты WP 4 и WP 5. На втором этапе выполнения проекта было принято решение о совмещении масштабируемых решений для предсказания уровня качества сервисных систем и уровня доверия к таким системам (четвертый и пятый рабочие пакеты), а также был предложен подход к прогнозированию обеих величин на основе специально синтезированных логических схем. Соответственно, на текущем этапе выполнения проекта мы, в первую очередь, остановились на программно-аппаратной реализации предложенного подхода. Пусть логические схемы LC1 и LC2 используются для предсказания значения QoE / предсказания уровня доверия (K) по двум заранее выбранным «эталонным» технологиям машинного обучения M1 и M2, причем алгоритм M1 детерминирован в сторону фиксированного ответа K из множества D1, в то время как алгоритм M2 достаточно хорошо классифицирует данные из множества D2. Значение K предлагается параллельно вычислять на обеих схемах LC1 и LC2, а далее на выходе схемы, вычисляющей значение K для композитного сервиса, воспользоваться подходящим мультиплексором для «снятия» требуемых выходов. Для аппаратной реализации модели машинного обучения в виде логической схемы подходят программируемые логические интегральные схемы (ПЛИС). Процесс программирования (и перепрограммирования) логических схем занимает считанные минуты с использованием программной среды Altera Quartus II и отладочной платы Altera Cyclone V GX Starter Kit, имеющей в своем составе ПЛИС Cyclone V GX 5cgxfc5c6f27c7n. Такая программно-аппаратная реализация для композитной логической схемы, описанной выше, была построена в 2018 г. В дальнейшем планируется интеграция подходящей FPGA реализации в телекоммуникационную сеть для «Интернета вещей» (IoT), где узлами выступают подходящие сенсоры, и распознавание ведется на сети из элементов с ограниченными вычислительными возможностями, т.е. устройств с небольшими ресурсами и вычислительной мощностью, которые создаются для специальных задач, например, IoT. Для подтверждения эффективности нашего подхода мы провели предварительные эксперименты, показавшие превосходство (в терминах скорости исполнения и потребления ресурсов) реализаций логических схем перед программными реализациями ряда методов машинного обучения, таких как искусственные нейронные сети (ANN или ИНС) и системы опорных векторов (SVM). Производительность логической схемы превосходит модель SVM в 424 раза. Производительность логической схемы (реализованной аппаратно) оказалась выше производительности нейронной сети примерно в 1000 раз. Интересным также представляется вопрос использования «неклассических» моделей машинного обучения, в частности, одна из компонент LC1 или LC2 может быть синтезирована напрямую, т.е. без обращения к операции моделирования эталонной модели обучения. Согласно проведенным экспериментам, наибольшее влияние на качество обучения рассмотренных самообучающихся моделей (логическая схема и ИНС) оказывает именно объём обучающей выборки. Вторым параметром выборки, на который необходимо обращать внимание, является среднее расстояние между опорными векторами выборки. Необходимо стараться «кластеризировать» опорные векторы, располагать их плотными группами. В этом случае можно рассчитывать на эффективный синтез логических схем-компонент, участвующих в вычислении результирующего значения QoE / уровня доверия. Тайваньский партнер также оценивает возможности эффективной реализации нейронной сети подходящей логической схемой. Акцент делается на ИНС, у которых узлы скрытых слоев соединены по принципу «каждый с каждым»; рассматривается случай двоичных входных / выходных наборов. При условии, что каждый из нейронов имеет подходящую аппаратную реализацию, ставится цель оптимизировать число связей в результирующей схеме. На последнем семинаре, проведенном в Национальном Университете Тайваня (октябрь 2018 г.), были начаты совместные обсуждения по предложению комбинированного (оконного или window) подхода на основе имеющегося задела двух научных групп. В частности, были поставлены следующие задачи: 1) определить свойства выделяемого фрагмента и условия «вырезания» нейронной подсети для дальнейшего моделирования; 2) определить композицию Verilog описания или AIG графа с подходящей аппаратной реализацией нейронной сети, полученной после оптимизации внутренних связей; 3) исследовать «независимость» двух и более фрагментов нейронной сети, которые могут быть промоделированы и оптимизированы параллельно и др. Результаты, полученные в процессе выполнения работ по проекту, опубликованы в 18 работах, в том числе, 1 монография, 8 – в журналах и периодических изданиях (2 входят в международные базы цитирования Scopus и Web of Science и 6 – в Перечень ВАК), 9 – в трудах международных конференций (8 входят в международные базы цитирования Scopus и Web of Science и 1 совместная публикация с Тайваньским партнером), сделано более 15 докладов на конференциях и семинарах различного уровня, в том числе, международных. Таким образом, в 2018 г. был получен ряд научных результатов мирового уровня; разработанные методы и алгоритмы были опробованы на элементах сервисных систем, проведенные эксперименты подтвердили их эффективность. Полученные результаты и возможные направления дальнейшей работы обсуждались на семинарах в Тайбэе, в частности, с целью продолжения совместных исследований и возможности подачи заявки на грант РНФ-MOST 2019 года.