Automation of Porting Android Applications to the HarmonyOS NEXT Ecosystem Using Formal Specifications

In recent years, there has been a trend in the mobile operating system market towards the creation of alternative platforms focused on proprietary programming languages and development tools. Companies are striving to reduce their dependence on existing solutions based on Android and iOS by developing their own ecosystems. One example of this approach is Huawei's HarmonyOS NEXT, which is completely abstracted from the Android OS and operates within its own ecosystem, including original programming languages, development environments, and an independent app store. The price for this independence in the initial phase is the lack of user applications: while Android and iOS have millions of applications, HarmonyOS NEXT has only a few thousand. Clearly, the issue of populating the ecosystem with applications is a very relevant task. This paper proposes an approach to populating the HarmonyOS NEXT ecosystem through automated porting of Android applications. The approach involves the systematic translation of components from the original Kotlin application into corresponding ArkTS components, which are native to client applications in HarmonyOS NEXT, while preserving the original logic and program structure. The most challenging component to port is libraries. To address this, the paper uses an automation approach for porting libraries based on specifications defined in the LibSL language. The observable behavior of Android and HarmonyOS NEXT libraries is described using behavioral specifications, which are then used to verify the logical compatibility of the two libraries. If compatible, an ArkTS library call chain is synthesized to replace the original Kotlin library call. Compatibility checking and synthesis are performed using an SMT solver. The proposed approach was implemented as a prototype tool, which was tested on simple Android applications. The tested applications were successfully ported to equivalent ArkTS applications with identical behavior.

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.