Автоматизация портирования 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.

1. Алексюк, А.О., Ицыксон, В.М. Семантически-ориентированная миграция Java-программ: опыт практического применения. Modeling and Analysis of Information Systems, 2017, 24, 677-690.

2. Перцев П.В. Использование формальных спецификаций для автоматизации портирования программ: выпускная квалификационная работа (магистр) / Перцев П.В.; науч. рук. Ицыксон В.М. Санкт-Петербург: Университет ИТМО, 2023. 2025 с.

3. JetBrains, Kotlin Analysis API, Available at: https://github.com/Kotlin/analysis-api, accessed 01.11.2025.

4. Huawei, Learning ArkTS. Available at: https://developer.huawei.com/consumer/en/doc/harmonyos-guides/learning-arkts, accessed 01.11.2025.

5. Itsykson V.M. LibSL: Language for Specification of Software Libraries, 2018.

6. de Moura L.M., Bjørner N.S. Satisfiability modulo theories. Communications of the ACM, 2011, vol. 54, no. 9, pp. 69-77. DOI: 10.1145/1995376.1995394.

7. Petrov M., Gagarski K., Belyaev M., Itsykson V. Using a Bounded Model Checker for Test Generation: How to Kill Two Birds with One SMT-solver. Modeling and Analysis of Information Systems, 2014, vol. 21(6), pp. 83-93 (in Russian). DOI: 10.18255/1818-1015-2014-6-83-93.

8. JetBrains, Kotlin/JS Compiler. Available at: https://kotlinlang.org/docs/js-overview.html, accessed 01.11.2025.

9. Gong L., Wang C., Cui D., Huang Y., Wei M. UITrans: Seamless UI Translation from Android to HarmonyOS. Proceedings of the 16th International Conference on Internetware, 2024.

10. Liu R., Lin Y., Hu Y., Zhang Z., Gao X. LLM-Based Java Concurrent Program to ArkTS Converter.

11. 39th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2024, pp. 2403-2406.