Автоматизация портирования Android-приложений в экосистему HarmonyOS NEXT с использованием формальных спецификаций

Автоматизация портирования Android-приложений в экосистему HarmonyOS NEXT с использованием формальных спецификаций

Миленин И.А. (Университет ИТМО, Санкт-Петербург, Россия)
Ицыксон В.М. (Университет ИТМО, Санкт-Петербург, Россия)

Аннотация

В последние годы на рынке мобильных операционных систем наблюдается тенденция создания альтернативных платформ, ориентированных на собственные языки программирования и инструменты разработки. Компании стремятся снизить зависимость от существующих решений на базе операционных систем (ОС) Android и iOS, развивая собственные экосистемы. Одним из примеров подобного подхода является система HarmonyOS NEXT компании Huawei, которая полностью абстрагировалась от ОС Android и функционирует в собственной экосистеме, включающей в свой состав оригинальные языки программирования, собственные среды разработки и независимый магазин приложений. Платой за независимость на первом этапе является является бедное наполнение пользовательскими приложениями: для Android и iOS количество приложений измеряется миллионами, а для Harmony OS NEXT – несколькими тысячами. Очевидно, что проблема наполнения экосистемы приложениями является очень актуальной задачей. В данной работе предлагается подход к наполнению экосистемы HarmonyOS NEXT путем автоматизированного портирования Android-приложений. Подход заключается в систематической трансляции компонентов исходного Kotlin-приложения в соответствующие компоненты на языке программирования ArkTS, являющимся нативным для клиентских приложений в HarmonyOS NEXT, с сохранением исходной логики и структуры программы. Самым сложным для портирования компонентом являются библиотеки. Для их переноса в работе применяется подход автоматизации портирования библиотек на основе спецификаций, заданных на языке LibSL. Видимое поведение библиотек Android и HarmonyOS NEXT описывается в виде поведенческих спецификаций, на основе которых проверяется логическая совместимость двух библиотек и, в случае успеха, синтезируется цепочка вызовов ArkTS-библиотеки, заменяющая исходный вызов библиотеки Kotlin. Проверка совместимости и синтез осуществляются с привлечением SMT-солвера. Предложенный подход был реализован в виде прототипа инструмента, который был апробирован на простых Android-приложениях. Тестируемые приложения были успешно портированы в эквивалентные по поведению приложения ArkTS.

Ключевые слова

операционная система HarmonyOS NEXT; язык программирования ArkTS; язык программирования Kotlin; портирование исходного кода; формальные спецификации; язык спецификации LibSL; решатель SMT Solver.

Издание

Труды Института системного программирования РАН, том 38, вып. 3, часть 4, 2026, стр. 83-100.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2026-38(3)-48

Для цитирования

Миленин И.А., Ицыксон В.М. Автоматизация портирования Android-приложений в экосистему HarmonyOS NEXT с использованием формальных спецификаций. Труды Института системного программирования РАН, том 38, вып. 3, часть 4, 2026, стр. 83-100. DOI: 10.15514/ISPRAS-2026-38(3)-48.

Полный текст статьи в формате pdf Вернуться к содержанию тома