Automation of porting Android applications to the HarmonyOS NEXT ecosystem using formal specifications

Automation of porting Android applications to the HarmonyOS NEXT ecosystem using formal specifications

Milenin I.A. (ITMO University, St. Petersburg, Russia)
Itsykson V.M. (ITMO University, St. Petersburg, Russia)

Abstract

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.

Keywords

HarmonyOS NEXT; ArkTS; Kotlin; source code porting; formal specifications; LibSL; SMT Solver.

Edition

Proceedings of the Institute for System Programming, vol. 38, issue 3, part 4, 2026, pp. 83-100

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

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

For citation

Milenin I.A., Itsykson V.M. Automation of porting Android applications to the HarmonyOS NEXT ecosystem using formal specifications. Proceedings of the Institute for System Programming, vol. 38, issue 3, part 4, 2026, pp. 83-100 DOI: 10.15514/ISPRAS-2026-38(3)-48.

Full text of the paper in pdf (in Russian) Back to the contents of the volume