Просмотр исходного текста страницы Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024)

;{{SpeakerInfo}}: {{Speaker|Александр Дельман}}
<blockquote>
Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов 
преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения. 

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

Изначально конвертер, включающий эти методы, представлял собой групповую лабораторную работу; 
в дальнейшем в проект добавились результаты также нескольких курсовых работ. 
</blockquote>

{{VideoSection}}

{{vimeoembed||800|450}}
{{youtubelink|}}

{{SlidesSection}}
[[File:Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024).pdf|left|page=-|300px]]

{{----}}

== Thesis ==
* https://github.com/OnionGrief/Chipollino

Современная теория формальных языков — фундамент для освоения теории компиляторов, теории типов, алгоритмов 
преобразования и анализа программ. Однако в части наглядных средств её освоения есть некоторые затруднения. 

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

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

Основные требования, предъявляемые к разработке:
;наглядность: — результаты преобразований должны быть представлены в понятной пользователю форме.  
Для решения этой задачи в качестве базового представления сущностей был выбран язык <tt>LaTeX</tt> и  библиотека \textsc{Tikz} для отрисовки автоматов. Эти средства наиболее выразительны, и из \LaTeX-формата нетрудно извлечь более простые посредством упрощающих гомоморфизмов.
;расширяемость: — интерфейс должен быть достаточно удобен для пополнения новыми функциями и типами автоматов или других представлений формальных языков. Для решения этой задачи конвертер был спроектирован таким образом, чтобы модули синтаксического разбора, проверки типов и логирования допускали обновления посредством автоматического порождения необходимого кода (исключая «рабский труд» по написанию шаблонного кода).
;связность: — должна быть возможность демонстрации соотношений между преобразованиями, а также их композициями. Для решения этой задачи было введено понятие цепочки преобразований, а также введены метод <tt>Verify</tt> (в пользовательском интерфейсе) и метаморфное тестирование<ref name="MetaTest"><i>T.&nbsp;Y.&nbsp;Chen, S.&nbsp;C.&nbsp;Cheung, S.&nbsp;M.&nbsp;Yiu</i>: Metamorphic testing: A new approach for generating next test cases // TR HKUST-CS98-01, Department of Computer Science, The Hong Kong University of Science and Technology, Hong Kong, 1998.</ref> (для разработчиков).   

=== Экосистема проекта ===

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

Сам конвертер написан на языках <tt>C++</tt>} (большая часть фронтенда и весь бэкенд) и <tt>Refal-5</tt> (форматирующие скрипты для порождения \LaTeX-исходников). В связи с этим, отдельно стоит упомянуть экспериментальный проект Линтера для <tt>Refal-5</tt>, 
который служит цели улучшить дисциплину кода, ранее не контролировавшуюся никем, кроме самого разработчика, делающего коммиты, 
и находится на стадии встраивания в «CI» проекта.

=== Применение в исследованиях ===

Хотя изначально конвертер разрабатывался как чисто учебный проект, оказалось, что этот инструмент удобен и 
для теоретических исследований. В частности, посредством метода <tt>Verify</tt> удобно перепроверять 
утверждения на предмет неявных допущений, что показал анализ статьи <ref name="Mohri"><i>C.&nbsp;Allauzen, M.&nbsp;Mohri</i>: A Unified Construction of the Glushkov, Follow,
and Antimirov Automata // TR2006-880, Courant Institute of Mathematical Sciences, 2006.</ref>, выявивший несколько неточностей 
в приведённых формулировках. Кроме того, методы анализа полугрупповых структур показали хорошую скорость и 
точность при выявлений «REDoS»-ситуаций в академических регулярных выражениях с перекрытиями в 
подвыражениях<ref name="SYRCoSE23"><i>A.&nbsp;N.&nbsp;Nepeivoda, Yu.&nbsp;A.&nbsp;Belikova, K.&nbsp;K.&nbsp;Shevchenko, M.&nbsp;R.&nbsp;Teriukha, D.&nbsp;P.&nbsp;Knyazihin, A.&nbsp;D.&nbsp;Delman, A.&nbsp;S.&nbsp;Terentyeva</i> REDoS detection in ``Domino'' regular expressions by Ambiguity Analysis // Труды ИСП РАН 35(3), 109—124, 2023.</ref>, для которых методы анализа, использующие самопересечения автоматов <ref name="RSA"><i>N.&nbsp;Weideman, B.&nbsp;van der Merwe, M.&nbsp;Berglund, B.&nbsp;W.&nbsp;Watson</i>:{Analyzing Matching Time Behavior of Backtracking Regular Expression Matchers by Using Ambiguity of {NFA}} //Proc. of Implementation and Application of Automata - 21st International Conference, {Lecture Notes in Computer Science}, 9705, p.322—334, 2016.</ref>, 
работают слишком медленно, а фаззеры<ref name="ReScue"><i>Y.&nbsp;Shen, Y.&nbsp;Jiang, C.&nbsp;Xu, P.&nbsp;Yu, X.&nbsp;Ma, J.&nbsp;Lu</i>: {Re{S}cue: Crafting Regular Expression DoS Attacks} // Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering, 225—235, 2018.</ref>,<ref name="Revealer"><i>Y.&nbsp;Liu, M.&nbsp;Zhang, W.&nbsp;Meng</i>: {Revealer: Detecting and Exploiting Regular Expression Denial-of-Service Vulnerabilities} // Proceedings of the 2021 IEEE Symposium on Security and Privacy (SP), 1468—1484, 2021.</ref> — ненадёжно. Последним применением конвертера 
на данный момент стало исследование бисимуляций в конечных автоматах с памятью посредством аппроксимаций 
классическими конечными автоматами<ref name="SYRCoSE24"><i>A.&nbsp;N.&nbsp;Nepeivoda, A.&nbsp;D.&nbsp;Delman, A.&nbsp;S.&nbsp;Terentyeva</i> Bisimulations in Memory Finite Automata // SYRCoSE 2024 Proceedings, 2024.</ref>. Поставленная цель — сделать осязаемыми абстрактные концепции, используемые в современной теории формальных языков, — оказалась полезна не только для сдачи 
зачётов, но и для испытания новых гипотез. 

{{----}}
[[File:{{#setmainimage:Chipollino — как лабораторная работа превратилась в инструмент для исследований (Александр Дельман, OSEDUCONF-2024)!.jpg}}|center|640px]]
{{LinksSection}}
<!-- <blockquote>[©]</blockquote> -->

<references/>

[[Категория:OSEDUCONF-2024]]
[[Категория:Draft]]
[[Категория:СПО в образовании]]